Mathematical Knowledge Management Across Formal Libraries
Mathematisches Wissensmanagement Über Formale Bibliotheksgrenzen Hinaus
Der Technischen Fakultät der Friedrich-Alexander-Universität Erlangen-Nürnberg zur Erlangung des Doktorgrades
Doktor-Ingenieur
vorgelegt von
Dennis Müller
aus
Garmisch-Partenkirchen
Als Dissertation genehmigt von der Technischen Fakultät der Friedrich-Alexander-Universität Erlangen-Nürnberg
|
Tag der mündlichen Prüfung:
|
18.10.2019
|
|
|
|
|
Vorsitzender der Promotionsorgans:
|
Prof. Dr.-Ing. Andreas Paul Fröba
|
|
Gutachter:
|
Prof. Dr. Michael Kohlhase
|
|
|
assoz. Prof. Dr. Claudio Sacerdoti Coen
|
This dissertation is concerned with the problem of integrating formal libraries: There is a plurality of theorem prover systems and related software with different strengths and weaknesses, that are fundamentally incompatible. This is due to different input languages, IDEs, library management facilities etc., but also due to fundamental theoretical aspects; primarily the reliance on different logical foundations, such as set theories, type theories, and additional primitive features (e.g. subtyping, specific module systems,...).
This thesis describes the approach towards solving this problem pursued at our research group. Specifically, it is divided into three main parts:
1.
2.
3.
(a)
(b)
(c)
(d)
Diese Doktorarbeit widmet sich dem Integrationsproblem formaler Bibliotheken: Es gibt eine Vielzahl an Theorembeweisern und verwandter formaler Software mit unterschiedlichen Stärken und Schwächen, die grundlegend inkompatibel sind. Dies liegt sowohl an unterschiedlichen Eingabesprachen, IDEs, Bibliotheksmanagement etc., als auch grundlegenden theoretischen Aspekten; primär die Verwendung unterschiedlicher logischer Fundamente, wie Mengentheorien, Typentheorien, und zusätzlichen primitiven Features (z.B. Subtyping, spezifische Modulsysteme,...).
Die Arbeit beschreibt den von unserer Forschungsgruppe verfolgten Ansatz, dieses Problem anzugehen. Konkret ist sie in drei zentrale Abschnitte geteilt:
1.
2.
3.
(a)
(b)
(c)
(d)
I am deeply indebted to the following people, who all contributed in some way to my success in – and/or well-being during – the writing of this thesis:
First and foremost my parents, for their unconditional support in all my endeavours, no matter how seemingly misguided.
My wonderful girlfriend Tina, for her unrestrained love and affection, and for happily playing Tropico next to me when I need to get work done while being with her.
My band mates in Vroudenspil, for providing me with a desperately needed outlet outside of my profession, besides being genuinely lovely friends to have. # ShamelessPlug
Many researchers I had the pleasure to meet, and who any inspired, taught, advised, humoured, supported, entertained, just generally have been extremely nice to me in various ways; including but not limited to: Jacques Carette, Merlin Carl, Claudio Sacerdoti Coen, Paul-Olivier Dehaye, Bill Farmer, Michael Junk, Cezary Kaliszyk, Peter Koepke, Andrea Kohlhase, Thomas Koprucki, Markus Pfeiffer, Natarajan Shankar, Nicolas Thiéry, Makarius Wenzel, ...
My colleagues at KWARC, for contributing to establishing a productive, and yet unusually comfortable and fun work environment: Katja Berčič, Jonas Betzendahl, Deyan Ginev, Mihnea Iancu, Constantin Jucovschi, Theresa Pollinger, Max Rapp, Frederik Schaefer, Tom Wiesing.
In particular Florian Rabe, who acted as a second advisor, especially in technical matters, and helped me literally every step of the way.
And last but not least Michael Kohlhase, for being an exceptionally passionate, caring and inspiring advisor, and for avoiding without exception all negative tropes about PhD advisors that make up the central plots of countless horror stories that traumatized post grads tell each other huddled around bonfires made from th revisions of (ultimately failed) thesis drafts.
“You don’t have to have a dream. Americans on talent shows always talk about their dreams. Fine, if you have something you’ve always wanted to do, dreamed of, like, in your heart, go for it. After all, it’s something to do with your time, chasing a dream. And if it’s a big enough one, it’ll take you most of your life to achieve, so by the time you get to it and are staring into the abyss of the meaninglessness of your achievement you’ll be almost dead, so it won’t matter.
I never really had one of these dreams, and so I advocate passionate dedication to the pursuit of short-term goals. Be micro-ambitious. Put your head down and work with pride on whatever is in front of you. You never know where you might end up. Just be aware, the next worthy pursuit will probably appear in your periphery, which is why you should be careful of long-term dreams. If you focus too far in front of you, you won’t see the shiny thing out the corner of your eye.”
“Don’t seek happiness. Happiness is like an orgasm: If you think about it too much it goes away. Keep busy and aim to make someone else happy, and you might find you get some as a side effect.”
“Be hard on your opinions. A famous bon mot asserts that opinions are like arseholes in that everyone has one. There is great wisdom in this, but I would add that opinions differ significantly from arseholes in that yours should be constantly and thoroughly examined.”
“Remember it’s all luck. You are lucky to be here. You are incalculably lucky to be born, and incredibly lucky to be brought up by a nice family that helped you get educated and encouraged you to go to uni.
Or, if you were born into a horrible family, that’s unlucky and you have my sympathy, but you are still lucky. Lucky that you happen to be made of the sort of DNA that went on to make the sort of brain which, when placed in a horrible childhood environment, would make decisions that meant you ended up eventually graduating uni. Well done, you, for dragging yourself up by your shoelaces. But you were lucky. You didn’t create the bit of you that dragged you up. They’re not even your shoelaces.
I suppose I worked hard to achieve whatever dubious achievements I’ve achieved, but I didn’t make the bit of me that works hard, any more than I made the bit of me that ate too many burgers instead of attending lectures when I was [at uni].
Understanding that you can’t truly take credit for your successes, nor truly blame others for their failures, will humble you and make you more compassionate.
Empathy is intuitive, but it is also something you can work on intellectually.”
Contents
3.1
LATIN25
6
LFX69
13
Conclusion147
13.1.3
Search149
14
Alignments157
15.3
Example180
16.1.2
Search187
Part I
Introduction
Chapter 1
Motivation
In the last decades, the formalization of mathematical knowledge (and the verification and automation of formal proofs) has become of ever increasing interest. Formal methods nowadays are not just used by computer scientists to verify software and hardware as well as in program synthesis, but – due to problems such as Kepler’s conjecture [Hal+15a], the classification theorem for finite simple groups [Sol95], etc. – are also becoming increasingly popular among mathematicians in general.
By now, there is a vast plurality of formal systems and corresponding libraries to choose from. However, almost all of these are non-interoperable, because they are based on differing, mutually incompatible logical foundations (e.g. set theories, higher-order logic, variants of type theory etc.), library formats, library structures, and much work is spent developing the respective basic libraries in each system.
Moreover, since a library in one such system is not reusable in another system, developers are forced to spend an enormous amount of time and energy developing basic library organization features such as distribution, browsing/search or change management for each library format; all of which binds resources that could be used to improve core functionality and library contents instead.
One reason for the incompatibility is the widespread usage of the homogeneous method, which fixes some logical foundation with all primitive notions (e.g. types, axioms, inference rules) and uses conservative extensions of this foundation to allow for modeling some specific domain knowledge. While homogeneous reasoning is conveniently implementable and verifiable, it implies that a lot of work is needed just to model the basic domains of discourse necessary for mathematics, such as real numbers, algebraic theories, etc. Moreover, the resulting formalizations are actually less valuable to mathematicians, since they are intimately dependent on (and framed in terms of) the underlying logic, making it virtually impossible to move the results between different foundations or to abstract from them.
In contrast, mathematical practice favors the heterogeneous method, as exemplified by the works of Bourbaki [Bou64]. In heterogeneous reasoning, theories are used to introduce new primitive notions and the truth of some proposition is relative to a theory (as opposed to absolute with respect to some foundation). This method is closely related to the “little theories” paradigm [FGT92a] which prefers to state each theorem in the weakest possible theory, thus optimizing reusability of mathematical results. Even though in theory, all of mathematics can be reduced to first principles – most prominently first-order logic with (some extension of) ZFC – it is usually carried out in a highly abstract setting that hides the foundation, often rendering it irrelevant and thus allowing it to be ignored.
Correspondingly, there is an inconvenient discrepancy between the currently existing formal libraries and the way (informal) mathematics is usually done in practice. Furthermore, the available formal knowledge is distributed among dozens of different mutually incompatible formal library systems with considerable overlap between them.
Additionally, [Car+19] recently introduced the five aspects of big math systems – aspects of doing mathematics that can and should be supported by software, collectively referred to as tetrapod, as in Figure 1.1. These aspects are
1.
2.
3.
4.
A
T
E
X and other text formating software with strong support for mathematical expressions, and finally 5.
Most software systems focus on one of those tetrapod aspects, few on two, and none strongly support all of them. That is despite the fact that all five of these aspects are intrinsic and important parts of doing real-world mathematics, and it is correspondingly vital to support all of them in an interconnected workflow.
What we should consequently aim for is a universal archiving solution for all formal knowledge, that
1.
2.
3.
4.
The aim of this thesis is to describe our approach to achieving such an archiving solution by integrating the libraries of existing software systems, focusing on the inference, computation, tabulation and organization aspects of the tetrapod, and to demonstrate its feasibility.
Chapter 2
State of the Art
The attempt to systematically formalize both mathematical knowledge and its semantics goes back at least to the seminal work by Bertrand Russell and Albert North Whitehead [WR13]. In the 1950s and 1960s, computer systems were added to the tool chest for this endeavour, shifting the focus to designing foundations that combine both machine-friendliness and human readability. This enabled automated theorem proving, thanks to ideas going back to Allen Newell, Herbert A. Simon, and Martin Davis. This has been most succesful for first-order logic and related systems. For more expressive languages, the verification of human-written formal proofs has been the more successful approach, going back to John McCarthy, Nicolaas Govert de Bruijn, Robin Milner, and Per Martin-Löf. Modern proof assistants usually combine both approaches, generally verifying user input interactively and employing automation for routine proof steps whenever possible.
Since developing sophisticated proof systems requires both a lot of practical work and a high level of theoretical knowledge, most popular proof assistants have invested a large amount of time and energy into building their systems. Consequently, formalization within one such system pays off mostly at large scales, calling for a community effort to extend the corresponding formal libraries. In practice, however, the availability of many different and mutually incompatible systems – each with their own advantages and disadvantages – has instead driven towards ever increasing specialization within the formal mathematics community, resulting in lots of different libraries with considerable (and from a heterogeneous point of view unnecessary) overlap of actual content.
A more extensive summary of the state of the art and the scientific context of this work can be found in [KR16b].
2.1Foundations
OverviewThe notion of a foundation goes back to the foundational crisis of mathematics at the beginning of the 20th century. Resulting from a general confusion regarding the ontological status of informally defined objects like infinitesimals in real analysis, non-euclidean geometries and sets as objects of study in their own right, as well as debates over the validity of certain non-constructive proof techniques of ever growing abstraction and intricacy, the idea developed to find a formal, logical basis that fixes both an ontology as well as an unambiguous notion of what constitutes a valid proof.
By now, it is generally accepted within the mathematical community, that the answer to this problem is the combination of first-order logic and some system of set theory, usually considered as (possibly extensions of) Zermelo-Fraenkel set theory with the axiom of choice (ZFC). However, already going back to Principia Mathematica by Russell and Whitehead (which can be seen as an early variant of type theory), alternative foundations have been around.
There’s an inherent trade-off in every such foundation with respect to their complexity and expressiveness. Theoretically, a foundation should be simple with very few primitive notions, to make reasoning about the foundation more convenient and establish trust in its consistency. On the other hand, since a foundation should ultimately establish a framework for all of mathematics, it should be as expressive as possible to allow mathematicians to talk about all of the desired objects and realms in terms of the foundation. This trade-off naturally lead to a large diversity of different foundations, which nowadays are used in different proof assistants.
All of these systems fix one specific foundation as a basis for their specification language, usually variants of either constructive type theory, higher-order logic or (as implicitely used in mathematics) first-order set theory. The constructive type theories are mostly based on Martin-Löf type theory [ML74] or the calculus of constructions [CH88] and make use of the Curry-Howard correspondence [CF58; How80] to treat propositions as types (and proofs as -terms). Systems include Nuprl [Con+86], Agda [Nor05], Coq [Tea03], and Matita [Asp+06a]. The second group of systems go back to Church’s higher-order logic [Chu40] and include HOL4 [HOL4], ProofPower [Art], Isabelle/HOL [NPW02], and HOL Light [Har96].
Since type theories and higher-order logics are more conveniently machine implementable, systems using set theories are noticably rarer. These are e.g. Mizar [Miz], Isabelle/ZF [PC93], and Metamath [MeMa].
The foundation of the PVS system (see Section 10.1) includes a variant of higher-order logic, but has been specifically designed to have a set theoretic semantics. The IMPS system [FGT93] is based on a variant of higher-order logic with partial functions. The foundation of ACL2 [KMM00] is an untyped language based on Lisp.
Heterogeneous ReasoningAs mentioned in the previous section, even though all of mathematics is assumed to be reducible to some foundation, the way mathematics is usually practiced is according to the heterogeneous method, in which all foundational aspects are “hidden” and left implicit, unless necessary in the respective context. One major advantage of this method, in which theories are used to introduce new primitive notions, is that (in connection with the little theories approach) it allows for reusing mathematical results and moving them along theory morphisms (i.e. truth-preserving maps) between theories. This approach has been applied successfully in software engineering and algebraic specification, where formal module systems are used to build large theories out of little ones, e.g., in SML [Mil+97] and ASL [SW83].
To accomodate for this more convenient style of reasoning, most formal systems have specific features that introduce some form of heterogeneity either explicitely or implicitely. Explicit features include e.g. “locales” in Isabelle, “parametric theories” in PVS, “modules” in Coq, or “structures” in Mizar. The IMPS system [FGT93] is somewhat unique in so far, as it was designed specifically with heterogeneous reasoning in mind.
To use the heterogeneous method implicitly, the user introduces a new formal construct (such as real numbers) by defining them in terms of existing ones (e.g. the usual construction via equivalence classes on Cauchy sequences) and proving the actually relevant (i.e. construction independent) theorems about them (e.g. field axioms, topological completeness). Finally, the user can rely on the proven properties alone, without ever needing to expand the concrete definition originally implemented, which in the process is rendered irrelevant for all practical purposes.
To enable implicit heterogeneity, the system has to provide corresponding definition principles. Examples include type definitions in the HOL systems, provably terminating functions in Coq or Isabelle/HOL, or provably well-defined indirect definitions in Mizar. However, it should be noted, that such implicit heterogeneous definitions are usually internally expanded into conservative extensions of the foundation. Alternatively, several data types provide an additional way to use heterogeneity implicitely. These include (Co)inductive types and record types e.g, as done by Mizar structures and with Coq records in the Mathematical Components project [MC]. This has the additional advantage, that it allows for computation within the foundation.
The Incompatibility ProblemThe homogeneous method (in combination with implicit heterogeneity) has an obvious advantage: Since the foundation is fixed and can not be extended by new axioms, the trusted code base remains fixed as well. Furthermore, is allows integrating computational methods e.g. to reason about equality, without having to tediously instantiate and apply the corresponding axioms. However, it has the major disadvantage of making reuse of formalized knowledge difficult, if not impossible. Since the techniques for implicit heterogeneity are elaborated on the basis of the foundation, the actual heterogeneous structure of some fragment of implemented knowledge is difficult to identify. Furthermore, since different systems offer different techniques to introduce implicit heterogeneity, the construction method used in one system can often not be easily translated into another system. Their elaborated implementations themselves are again framed in terms of the foundation (or an intrinsic part thereof), and are consequently useless for a system based on a differing foundation.
Even though a fixed foundation is therefore reasonable for an individual formal system, if we envision a universal library of mathematics – a major goal of formal mathematics going back at least to the QED project and manifesto [Qed] of 1994 – this is the wrong approach. Furthermore, different areas of mathematics favor different foundations (such as category theory, specifically in algebra), as do different communities dealing with formalizing mathematics, whether due to technical reasons or simply familiarity. Thus, formal libraries would profit from foundational pluralism, i.e., the ability to support multiple foundations in a single universal library.
2.2Formal Libraries
OverviewUsually, implemented formal systems have some notion of a library, a collection of formalizations (usually just the corresponding source files) that can be handled in specific ways – imported and used when creating new content, collectively exported, etc. Most systems are distributed with some base library providing the most useful and ubiquitous settings of interest, such as Booleans or number spaces, and often maintain additional, community-created libraries with more advanced contents.
The Isabelle and the Mizar groups maintain one centralized library each – the “Archive of Formal Proofs” [AFP] and the “Mizar Mathematical Library” [MizLib], respectively. The Coq group relies on a package manager on top of distributed Git repositories instead of a central archive. These libraries contain individual formalizations with relatively few interdependencies. Other libraries are generated and maintained by communities apart from the developers of the system, however, these are still often valuable in their own right, such as Tom Hales’s formalizations in HOL Light for the Kepler conjecture [Hal+15a] and Georges Gonthier’s work in Coq for the recently proved Feit-Thompson theorem [Gon+13]. John Harrison’s formalizations in his HOL Light system [Har96] and the NASA PVS library [PVS] have a similar flavor although they were not motivated by a single theorem but by a specific application domain. The latter is one of the biggest decentralized libraries, whose maintenance is disconnected from that of the system.
As mentioned, most of these systems are based on the homogeneous method. However, there are some libraries that are intrinsically heterogeneous, such as the IMPS library [FGT], the LATIN logic library [Cod+11] developed at KWARC (see Section 3.1) and the TPTP library [Sut09] of challenge problems for automated theorem provers. Unfortunately, none of these enjoy the level of interpretation, deduction, and computation support developed for individual fixed foundations.
The OpenTheory format [Hur09] offers some support for heterogeneity in order to allow moving theorems between systems for higher-order logic (specifically HOL Light, HOL4, and ProofPower). It provides a generic representation format for proofs within higher-order logic that makes the dependency relation (i.e., the operators and theorems used by a theorem) explicit. The OpenTheory library comprises several theories that have been obtained by manually refactoring exports from HOL systems.
Library IntegrationThere are two problems concerning library integration. The first is, given a single library, refactoring its contents to increase modularity. This results in a “more heterogeneous” set of theories, thus making it easier to reuse and blowing up the corresponding theory graph to make shared or inherited theories and results more visible and explicit. An attempt at giving a formal calculus for theory refactoring has recently been published [AH15].
The second, and for this thesis more relevant, problem is to integrate two or more given libraries with each other, so that knowledge formalized in one of them can be reused in, translated to or identified with contents of the others. In the best case, two libraries might even be merged into a single library with ideally no redundant content.
No strong tool support is available for any of these facets. The state-of-the-art for refactoring a single library is manual ad hoc work by experts, maybe supported by simple search tools (often text-based). Also, the widespread use of the homogeneous method makes integrating and merging libraries in different systems extremely difficult, since usually basic concepts in one foundation cannot be directly translated to corresponding concepts in the other [KRSC11].
This is despite the large need for more integrated and easily reusable large libraries. For example, in Tom Hales’s Flyspeck project [Hal+15a], his proof of the Kepler conjecture is formalized in HOL Light. But it relies on results achieved using Isabelle’s reflection mechanism, which cannot be easily recreated in HOL Light. And this is an integration problem between two tools based on the same root logic.
Library TranslationsThere are two ways to take on library integration. Firstly, one can try to translate the contents of one formal system directly into another system; I will call this a library bridge. This requires intimate knowledge of both systems and their respective foundations used, and is necessarily somewhat ad-hoc. A small number of library bridges have been realized, typically in special situations. [KW10] translates from HOL Light [Har96] to Coq [Tea03] and [OS06a] to Isabelle/HOL. Both translations benefit from the well-developed HOL Light export and the simplicity of the HOL Light foundation. [KS10] translates from Isabelle/HOL [NPW02] to Isabelle/ZF [PC93]. Here import and export are aided by the use of a logical framework to represent the logics. The Coq library has been imported into Matita [Asp+06a] once, aided by the fact that both use very similar foundations. The OpenTheory format [Hur09] facilitates sharing between HOL-based systems but has not been used extensively.
The second way is to use a more general logical framework (see Section 2.3) which provides some way to specify the respective foundations, and integrate the libraries under consideration directly into that framework. Then the framework can serve as a uniform intermediate data structure, via which other systems can import the integrated libraries. This approach will be extensively described in this thesis, using the logical framework LF [HHP93a] and making the libraries available to knowledge management services. Another example is the Dedukti system [BCH12], which imports, e.g., Coq and HOL Light into a similar logical framework, namely LF extended with rewriting.
Dedukti underlies the recent Logipedia project [DT], aiming to build an encyclopedia of formal proofs in simple type theory (originally developed in Matita), which can be exported to other systems.
Again, the prevalence of the homogeneous method constitutes a major problem here. Even with implicit heterogeneity, the fact that e.g. theories such as the real numbers are still modeled as conservative extensions of a fixed foundation using some intricate construction principle (cauchy sequences, Dedekind cuts) means, that using different definitions can make it impossible to align a theory in one library to the corresponding theory in a different library, even though from a mathematical point of view they are “the same” (i.e. isomorphic). And even if the same abstract construction principle is used in two libraries, their implementations in terms of the underlying foundation can be different enough to make it difficult to identify the two resulting theories.
Very little work exists to address this problem. In [OS06a], some support for library integration was present: Defined identifiers could be mapped to arbitrary identifiers ignoring their definition. No semantic analysis was needed because the translated proofs were rechecked by the importing system anyway. This approach was revisited and improved in [KK13a], which systematically aligned the concepts of the basic HOL Light library with their Isabelle/HOL counterparts and proved the equivalence in Isabelle/HOL. The approach was further improved in [GK14a] by using machine learning to identify large sets of further alignments.
The OpenTheory format [Hur09] provides representational primitives that, while not explicitly using theories, effectively permit heterogeneous developments in HOL. The bottleneck here is manually refactoring the existing homogeneous libraries to make use of heterogeneity.
A partial solution aimed at overcoming the integration problem was sketched in [RKS11].
2.3Logical Frameworks
Over the last 20 years, formal systems have added an additional metal level through the introduction of logical frameworks. These provide tools to specify logical systems themselves in a formal way. An overview of the current state of art is given by [Pfe01].
An example for one such framework is LF [HHP93a] (see Section 4.3). Logical frameworks introduce the possibility to additionally reason about logics, as e.g. in Twelf [PS99], which is the currently most mature implementation of LF. Twelf has been used as a basis for the LATIN library (see Section 3.1). Also, since in logical frameworks logics are themselves represented as theories, they allow for defining logical systems heterogeneously, by building them up in a modular way.
Dedukti [BCH12] implements LF modulo rewriting. By supplying rewrite rules (whose confluence Dedukti assumes) in addition to an LF theory, users can give more elegant logic encodings. Moreover, rewriting can be used to integrate computation into the logical framework. A number of logic libraries have been exported to Dedukti, which is envisioned as a universal proof checker. Isabelle [Isa] implements intuitionistic higher-order logic, which (if seen as a pure type system with propositions-as-types) is rather similar to LF. Despite being logic-independent, most of the proof support in Isabelle is optimized for individual logics defined in Isabelle, most importantly Isabelle/HOL and Isabelle/ZF.
Prolog – in its most mature implementation ELPI [Dun+15] – extends the logic programming paradigm with higher-order functionalities. As such, it allows higher-order abstract syntax approaches and can be (and is) used as a logical framework as well.
Unfortunately, logical frameworks are not an efficient alternative to the prevailing homogeneous formal systems. State of the art proof assistents rely heavily on the specific peculiarities of their underlying foundation to provide efficient proof search techniques, which would be impossible to implement at the high level of generality that logical frameworks provide, at least without introducing cosiderable overhead and thus reducing efficiency.
Another problem is that specific concepts used by some logic (noticably record types, subtyping principles, inductive definitions, etc.) may be difficult to realize in a logical framework in such a way, that type checking can be done effectively, since the necessary information for doing so can not always easily be lifted to the rather general level on which the type checker operates (see Part II).
Chapter 3
Context and Contribution
This thesis is part of two ongoing research projects - OAF (Open Archive of Formalizations) and ODK (OpenDreamKit). The goals of OAF in particular largely coincide with the objectives of this thesis, specifically regarding applications for theorem prover libraries; ODK entails work packages extending the same goals to other formal systems, such as computer algebra systems and mathematical databases. Our approach to realizing these projects largely make use of the Math-in-the-Middle architecture (MitM).
Before we describe the precise objectives and contribution of this work, we will go over the above and related projects, as to establish the necessary context.
3.1LATIN
The LATIN project [Cod+11] was a DFG funded project running from 2009 to 2012 under the principal investigators Michael Kohlhase, Florian Rabe and Till Mossakowski. Its aim has been to build a heterogeneous, highly integrated library of formalizations of logics and related languages as well as translations between them. It uses Mmt (see Section 4.1) as a framework, with the logical framework LF (see Section 4.3) as a meta-theory for the individual logics.
True to the general Mmt philosophy, all the integrated theories are built up in a modular way and include propositional, first-order, sorted first-order, common, higher-order, modal, description, and linear logics. Type theoretical features, which can be freely combined with logical features, include the -cube, product and union types, as well as base types like booleans or natural numbers. In many cases alternative formalizations are given (and related to each other), e.g., Curry- and Church-style typing, or Andrews and Prawitz-style higher-order logic. The logic morphisms include the relativization translations from modal, description, and sorted first-order logic to unsorted first-order logic, the negative translation from classical to intuitionistic logic, and the translation from first to sorted first- and higher-order logic.
The left side of Figure 3.1 shows a fragment of the LATIN atlas, focusing on first-order logic (FOL) being built on top of propositional logic (PL), its translation to HOL and ultimately resulting in the foundations of Mizar, Isabelle/HOL and ZFC, as well as translations between them. The formalization of propositional logic includes its syntax as well as its proof and model theory, as shown on the right of Figure 3.1.
3.2The OAF Project
The OAF project [OAF] is a DFG funded project running from 2015 to 2019 under the principal investigators Michael Kohlhase and Florian Rabe. The goal was to provide an Open Archive of Formalizations: a universal archiving solution for formal libraries, corresponding library management services (such as distributing, browsing and searching library contents) and methods for integrating libraries in different formalisms in a unifying framework – namely OMDoc/Mmt (see Section 4.1), as in Figure 3.2 – to allow for sharing and translating content across them. We further want it to be scalable with respect to both the size of the knowledge base and the diversity of logical foundations.
Theoretically, the main prerequisite has been established in the LATIN project (see Section 3.1). However, whereas LATIN provides formalizations of basic logics, type theories and related systems, there still remains the problem of integrating the existing formal libraries of theorem prover systems. Consequently, there are two major objectives of the OAF project this thesis touches on:
Making existing libraries accessible to a unifying frameworkWe want to be able to make available theorem prover libraries accessible to the Mmt system.
Libraries that have been imported into Mmt in the course of this project include HOL Light [KR14], Mizar [Ian+13], TPTP [Sut09], IMPS [Bet18], Coq [MRS], Isabelle (as-of-yet unpublished) and (as presented in detail in Chapter 10) PVS.
Refactoring and integrating librariesOnce we have several libraries integrated into Mmt, we can implement generic knowledge management services for the integrated libraries, such as:
•
•
Naturally, both aspects are heavily interrelated, since integrating libraries is easier after some suitable refactoring, and already aligned libraries can potentially be analyzed more easily and further refactored.
3.3OpenDreamKit
As with interactive theorem provers specifically, in the last decades we witnessed the emergence of a wide ecosystem of open-source tools to support research in pure mathematics in general. This ranges from specialized to general purpose computational tools such as GAP [Gro16], PARI/GP, LinBox, MPIR, Sage [Dev16], or Singular [SNG], via online databases like the LMFDB [LMF] or online services like Wikipedia, arXiv [Arx], to webpages like MathOverflow. A great opportunity is the rapid emergence of key technologies, in particular the Jupyter [Jup] (previously IPython) platform for interactive and exploratory computing which targets all areas of science.
This has proven the viability and power of collaborative open-source development models, by users and for users, even for delivering general purpose systems targeting large audiences such as researchers, teachers, engineers, amateurs, and others. Yet some critical long term investments, in particular on the technical side, are in order to boost the productivity and lower the entry barrier:
•
Streamlining access, distribution, portability on a wide range of platforms, including High Performance Computers or cloud services. •
Improving user interfaces, in particular in the promising area of collaborative workspaces as those provided by CoCalc [CC] (previously called SageMathCloud). •
Lowering barriers between research communities and promoting dissemination. For example make it easy for a specialist of scientific computing to use tools from pure mathematics, and vice versa. •
Bringing together the developer communities to promote tighter collaboration and symbiosis, accelerate joint development, and share best practices. •
Structure the development to outsource as much of it as possible to larger communities, and focus manpower on core specialities: the implementation of mathematical algorithms and databases. •
And last but not least: Promoting collaborations at all scales to further improve the productivity of researchers in pure mathematics and applications. OpenDreamKit – “Open Digital Research Environment Toolkit for the Advancement of Mathematics” [ODK] – is a project funded under the European H2020 Infrastructure call [EI] on Virtual Research Environments, to work on many of these problems.
In practice, OpenDreamKit’s work plan consists of several work packages: component architecture (modularity, packaging, distribution, deployment), user interfaces (Jupyter interactive notebook interfaces, 3D visualization, documentation tools), high performance mathematical computing (especially on multicore/parallel architectures), a study of social aspects of collaborative software development, and a package on data/knowledge/software-bases.
The latter package focuses on the identification and extension of ontologies and standards to facilitate safe and efficient storage, reuse, interoperation and sharing of rich mathematical data, whilst taking provenance and citability into account. This package is the most relevant regarding this thesis.
Its outcome will be a component architecture for semantically sound data archival and sharing, and integrate computational software and databases. The aim is to enable researchers to seamlessly manipulate mathematical objects across computational engines (e.g. switch algorithm implementations from one computer algebra system to another), front end interaction modes (database queries, notebooks, web, etc) and even backends (e.g. distributed vs. local).
3.4The Math-in-the-Middle Approach and Library
The Math-in-the-Middle architecture is used heavily in the OpenDreamKit project. It centers around the Math-in-the-Middle ontology, an Mmt archive of formalized math using all of the features introduced in Part II. In particular, this archive provides useful real-world examples for these features. The ontology serves as a mediator between individual systems involved in the OpenDreamKit project to facilitate knowledge exchange and remote procedure calls.
Additionally, the Math-in-the-Middle architecture can be used in other contexts. In particular, it facilitates across-library knowledge management services for formal libraries, as described in Part IV. From this perspective, while this section focuses on the role of the architecture in the OpenDreamKit project, the general ideas underlying this section can be generalized beyond the systems involved in OpenDreamKit.
Since we aim to make our components interoperable at a mathematical level, we have to establish a common meaning space that will allow us to share computation, visualization of the mathematical concepts, objects, and models between the respective systems. This mediation problem is well understood in information systems [Wie92], and has for instance been applied to natural language translation via a hub language [KW03]. Here, our hub is mathematics itself, and the vocabulary (or even language) admits further formalization that translates into direct gains in interoperability. For this reason, neither OpenMath [Bus+04] nor MathML [Aus+03] have the practical expressivity needed for our intended applications.
3.4.1A Common Meaning Space for Interoperability
One problem is that the software systems in OpenDreamKit cover different mathematical concepts, and if there are overlaps, their models for them differ, and the implementing objects have different functionalities. This starts with simple naming issues (e.g. elliptic curves are named ec in the LMFDB, and as EllipticCurve in Sage), persists through the underlying data structures and in differing representations in the various tables of the LMFDB), and becomes virulent at the level of algorithms, their parameters, and domains of applicability.
To obtain a common meaning space for a VRE, we have the three well-known approaches in Figure 3.3.
The first does not scale to a project with about a dozen systems, for the third there is no obvious contender in the OpenDreamKit ecosystem. Fortunately, we already have a “standard” for expressing the meaning of mathematical concepts – mathematical vernacular: the language of mathematical communication, and in fact all the concepts supported in the OpenDreamKit VRE are documented in mathematical vernacular in journal articles, manuals, etc. The obvious problem is that mathematical vernacular is too i) ambiguous: we need a human to understand structure, words, and symbols ii) redundant: every paper introduces slightly different notions.
Therefore we explore an approach where we flexiformalize (i.e. partially formalize; see [Koh13a]) mathematical vernacular to obtain a flexiformal ontology of mathematics that can serve as an open communication vocabulary. We call the approach the Math-in-the-Middle (MitM) Strategy for integration and the ontology the MitM ontology.
The descriptions in the MitM ontology must simultaneously be system-near to make interfacing easy for systems, and serve as an interoperability standard – i.e. be general and stable. If we have an ontology system that allows modular/structured ontologies, we can solve this apparent dilemma by introducing interface theories [KRSC11], i.e. ontology modules (the light purple circles in Figure 3.4) that are at the same time system-specific in their description of mathematical concepts – near the actual representation of the system – and part of the greater MitM ontology (depicted by the cloud in Figure 3.4) as they are connected to the core MitM ontology (the blue circle) by views we call interface views. The MitM approach stipulates that interface theories and interface views are maintained and released together with the respective systems, whereas the core MitM ontology represents the mathematical scope of the VRE and is maintained with it. In fact in many ways, the core MitM ontology is the conceptual essence of the mathematical VRE.
Apart from OpenDreamKit, the MitM ontology is furthermore used in the FrameIT [RKM16] approach for developing serious games for math education, and the MaMoRed project ([Koh+17b],[Kop+18]) with the goal of building a modular library of computational models in physics and related STEM fields.
3.5Objectives
The OAF and OpenDreamKit projects have a common aim, differing only in their domains of applicability – or aspects of the tetrapod (see Chapter 1): The integration of (libraries of) formal systems (inference) in the former, and mathematical software and databases (computation/tabulation) in the latter. The goal of this thesis is to outline an approach to solve this integration problem and to demonstrate its feasibility. This entails the following objectives:
O1
O2
O3
3.6Contribution and Overview
In Part II, I present a modular logical framework (O2) that extends LF by various features and is used in the remainder of this work. In particular, I explain in detail how we can use Mmt to develop such a framework and extend it by virtually arbitrary additional features via various means. Where issues arise (e.g. with advanced subtyping principles, see Chapter 7), I discuss these and suggest solutions.
Notably, unlike other fixed-foundation frameworks, we can do so without needing to express our principles in terms of a more primitive logic. Instead, we can use the conveniences of an extensive API providing all of the necessary and most common abstractions in a modern, production-ready programming language (Scala) and all the infrastructure that comes with it – such as modern IDEs with static type checking and debugging functionality, extensive library support, etc.
In Part III I demonstrate the OAF (and partially ODK) approach to integrating libraries and ontologies into the Mmt system (O1), using the theorem prover system PVS (Chapter 10), the computer algebra systems GAP and Sage (Chapter 12), and the database LMFDB (Chapter 11) as representative examples. The formalization of the foundational logic of PVS in Section 10.2 in particular requires and makes use of the logical framework presented in Part II. Since that logical framework is easily extendable – and since PVS can be considered particularly challenging as evidenced by the fact that no earlier representations of the PVS foundation exist in other frameworks – the approach likely scales to virtually arbitrary systems and their foundations.
As a result, we have, for the first time, all symbols from both the underlying foundations and ontologies as well as the associated libraries of formal systems accessible from within the same framework. In particular, we preserve the original presentation and semantics without the need to build dedicated (and sometimes impossible or unsound) translations between foundations.
Finally, Part IV covers knowledge management services (O3) that can now be implemented generically and foundation-independently, and which are consequently available for any (pair of) systems integrated into Mmt now or in the future. In particular, I present:
•
•
•
•
The last four points particularly achieve the main goals of the OAF project, and ultimately enable the intended results of (our part of) the OpenDreamKit project. The translation method in particular allows for transfering virtually arbitrary formal content between libraries and foundations, thus facilitating e.g. remote procedure calls between systems – in other words, it allows for flexibly and fully integrating formal systems and their libraries.
As such, this thesis demonstrates the feasibility of our approach to library integration in enabling proper knowledge management beyond individual systems and libraries within a unifying framework and system, bringing us one step closer to a full tetrapodal system.
Consequently this work covers a broad spectrum, ranging from purely theoretical developments down to implementation details.
Much of the content of this thesis has been published in previous papers. These are listed separately in the bibliography (Section 18).
Chapter 4
Preliminaries
Throughout this thesis we will use the Mmt language and system as a meta-logical framework. Mmt is a highly flexible system and API using the foundation-independent OMDoc language for its backend. Within Mmt, we can implement almost arbitrary logical frameworks; most prominently, it comes with an implementation of LF which we extend and use throughout this thesis.
4.1OMDoc/Mmt
OMDoc [Koh13b] is a representation language developed by Michael Kohlhase, that extends OpenMath and MathML and allows for providing general definitions of the syntax of both mathematical objects as well as mathematical documents. They make use of content dictionaries, which introduce primitive notions and their semantics. In particular, it can represent exports of formal system libraries and their documentation.
In the last ten years, (chiefly) Florian Rabe redeveloped the fragment of OMDoc pertaining to formal knowledge resulting in the OMDoc/Mmt language [RK13a; HKR12a; Rab17b]. OMDoc/Mmt greatly extends the expressivity, clarifies the representational primitives, and formally defines the semantics of this OMDoc fragment. It is designed to be foundation-independent and introduces several concepts to maximize modularity and to abstract from and mediate between different foundations, to reuse concepts, tools, and formalizations.
More concretely, the OMDoc/Mmt language integrates successful representational paradigms
•
the logics-as-theories representation from logical frameworks, •
theories and the reuse along theory morphisms from the heterogeneous method, •
the Curry-Howard correspondence from type theoretical foundations, •
URIs as globally unique logical identifiers from OpenMath, •
the standardized XML-based interchange syntax of OMDoc, and makes them available in a single, coherent representational system for the first time. The combination of these features is based on a small set of carefully chosen, orthogonal primitives in order to obtain a simple and extensible language design.
OMDoc/Mmt offers vey few primitives, which have turned out to be sufficient for most practical settings (a more detailed grammar is given in Section 4.1.1). These are
1.
2.
3.
4.
Using these primitives, logical frameworks, logics and theories within some logic are all uniformly represented as Mmt theories, rendering all of those equally accessible, reusable and extendable. Constants, functions, symbols, theorems, axioms, proof rules etc. are all represented as constant declarations, and all terms which are built up from those are represented as objects.
Theory morphisms represent truth-preserving maps between theories. Examples include theory inclusions, translations/isomorphisms between (sub)theories and models/instantiations (by mapping axioms to theorems that hold within a model), as well as a particular theory inclusion called meta-theory, that relates a theory on some meta level to a theory on a higher level on which it depends. This includes the relation between some low level theory (such as the theory of groups) to its underlying foundation (such as first-order logic), and the latter’s relation to the logical framework used to define it (e.g. LF).
All of this naturally gives us the notion of a theory graph, which relates theories (represented as nodes) via vertices representing theory morphisms (as in Figure 4.1), being right at the design core of the OMDoc/Mmt language.
Given this modular approach of OMDoc/Mmt, heterogeneity is made explicit in the sense, that even though foundations are present via meta-theories, only those aspects of the foundation that are used in the definition of a theory are present in the theory itself, making it easy to abstract from the foundation and reuse the theory.
The OMDoc/Mmt language is used by the Mmt system [RK13a], which provides a powerful API to work with documents and libraries in the OMDoc/Mmt language, including a terminal to execute Mmt specific commands, a web server to display information about Mmt libraries (such as their theory graphs) and plugins for the text editors/IDEs jEdit and IntelliJ IDEA, that can be used to create, type check and compile documents into the OMDoc/Mmt language. The API is heavily customizable via plugins to e.g. add foundation specific type checking rules and import and translate documents from different formal systems.
All of this puts Mmt on a new meta level, which can be seen as the next step in a progression towards more abstract formalisms as indicated in the table below. In conventional mathematics (first column), domain knowledge is expressed directly in ad hoc notation. Logic (second column) provided a formal syntax and semantics for this notation. Logical frameworks (third column) provided a formal meta-logic in which to define this syntax and semantics. Now Mmt (fourth column) adds a meta-meta-level, at which we can design even the logical frameworks flexibly. (This meta-meta-level gives rise to the name Mmt with the last letter representing both the underlying theory and the practical tool.) That makes Mmt very robust against future language developments: We can, e.g., develop LF +X without any change to the Mmt infrastructure and can easily migrate all results obtained within LF.
|
|
|||
|
Mathematics
|
Logic
|
Meta-Logic
|
Foundation-Independence
|
|
|
|||
|
|
|
|
Mmt
|
|
|
|
logical framework
|
logical framework
|
|
|
logic
|
logic
|
logic
|
|
domain knowledge
|
domain knowledge
|
domain knowledge
|
domain knowledge
|
|
|
4.1.1Mmt Syntax
Intuitively, OMDoc/Mmt is a declarative language for theories and views over an arbitrary object language. For the purposes of this thesis, we will work with the (only slightly simplified)
grammar given in Figure 4.2.
In the simplest case, theories are lists of constant declarations , where is an expression that may use the previously declared constants. Naturally, must be subject to some type system (which MMT is also parametric in), for the purposes of this thesis primarily the logical framework LF (see Section 4.3) and extensions thereof.
Mmt achieves language-independence through the use of meta-theories: every Mmt-theory may designate a previously defined theory as its meta-theory. For example, when we represent the HOL Light library in MMT, we first write a theory for the logical primitives of HOL Light. Then each theory in the HOL Light library is represented as a theory with as its meta-theory. In fact, we usually go one step further: itself is a theory, whose meta-theory is a logical framework such as LF. That allows to concisely define the syntax and inference system of HOL Light.
Correspondingly, a view is a list of assignments of -expressions to -constants . To be well-typed, must preserve typing, i.e., we must have . Here is the homomorphic extension of , i.e., the map of -expressions to -expressions that substitutes every occurrence of a -constant with the -expression assigned by .
We call simple if the expressions are always -constants rather than complex expressions. The type-preservation condition for an assignment reduces to where and are the types of and . We call partial if it does not contain an assignment for every -constant and total otherwise.
Importantly, we can then show generally at the Mmt-level that if is well-typed, then preserves all typing and equality judgments over . In particular, if we represent proofs as typed terms (see Section 4.3), views preserve the theoremhood of propositions. This property makes views so valuable for structuring, refactoring, and integrating large corpora.
Syntactically:
•
•
•
It remains to define the exact syntax of expressions. In the grammar in Figure 4.2, refers to constants and refers to bound variables.
Simple expressions are either references to constants (of the meta-theory, an included theory or previously declared in the current theory) or to bound variables . Complex expressions are of the form , where
•
is the operator that forms the complex expression, •
declares a variable of type that is bound by in subsequent variable declarations and in the arguments, •
is an argument of The bound variable context may be empty, and we write instead of . For example, the axiom would instead be written as
To refer to constants (and modules), OMDoc/Mmt employs globally unique URIs, which are composed of a namespace, the name of the (containing) module and the name of a constant, separated by question marks.
Hence, Mmt URIs are triples of the form
The namespace part is a URI that serves as a globally unique root identifier of a corpus, e.g. . It is not necessary (although often useful) for namespaces to also be URLs, i.e., a reference to a physical location. But even if they are URLs, we do not specify what resource dereferencing should return. Note that because Mmt URIs use as a separator, is the query part of the URI, which makes it easy to implement dereferencing in practice.
The module and symbol parts of an Mmt URI are logically meaningful names defined in the corpus: The module is the container (i.e. a theory, view or advanced structural feature) and the symbol is a name inside the module (of a constant, include or more advanced feature). Both module and symbol name may consist of multiple /-separated segments to allow for nested modules and qualified symbol names.
Mmt URIs allow arbitrary Unicode characters. However, and , which are used as delimiters, as well as any character not legal in URIs must be escaped using the %-encoding (RFC 3986/7 standard).
By using URIs, namespaces have the great advantage of being guaranteed to be globally unique. This comes at the prize of being rather long. However, the CURIE standard can be used to introduce short prefixes.
Mmt offers an additional theory morphism that we will occasionally but rarely use in this thesis. A structure is a theory morphism that behaves like an include in that it makes all constants in accessible to . Unlike includes, however, structures
1.
2.
For simplicity in the remaining part of the paper we will rarely use complete HTTP links, but rather use single keyword abbreviations.
4.1.2MathHub
MMT is used as a backend for the MathHub system [Ian+14; MH] – an online portal for mathematical documents. It is available on and hosts various Mmt repositories, interfaces for browsing and semantic search [KŞ06], as well as several additional applications, such as the semantic glossary for mathematics (SMGLoM) [Gin+16].
Most of the specific OMDoc/Mmt formalizations in this thesis are hosted on MathHub’s GitLab instance () and linked accordingly.
4.2The Mmt API
The Mmt system works on content represented in a fragment of OMDoc, a fact that is reflected by the internal datastructures corresponding to the syntax stated in Figure 4.2. All expression-level syntactic constructs are implemented as Scala case classes extending the class Term, and are named after the corresponding XML nodes of the underlying OMDoc.
Mmt URIs (see Section 4.1.1) are implemented as objects of the class Path, which are assembled from individual path components of type LocalName. The relevant subtypes are DPath for namespaces, MPath for module URIs of the form (d : DPath) ? (ln : LocalName), and GlobalName for declaration URIs of the form (m : MPath) ? (ln : GlobalName).
Figure 4.3 gives a translation of the abstract syntax for expressions described above into the internal datastructures.
|
Abstract Syntax
|
Scala Syntax
|
|
|
|
|
Symbol References
|
OMID(S : ContentPath)
|
|
Module References
|
OMMOD(M : MPath)
= OMID(M)
|
|
Constant References
|
OMS(C : GlobalName)
= OMID(C)
|
|
Variable References
|
OMV(V : LocalName)
|
|
|
|
|
Applications
|
OMA(f : Term, args : List[Term])
|
|
Binding Applications
|
OMBIND(f : Term, con : Context, arg: Term)
|
|
|
|
|
Context
|
Context(vars : List[VarDecl])
|
|
Variable Declaration
|
VarDecl(v : LocalName, t : Option[Term], d : Option[Term])
|
Figure 4.3: Internal Scala Datastructures for Mmt Syntactical Constructors
For a detailled and up-to-date description of the classes provided by the Mmt API, I refer to the Mmt documentation.
4.2.1Judgments
Mmt has a component called solver, parametrized by rules, that checks judgments and infers implicit arguments (solving placeholder variables). The solver uses a bidirectional type system, i.e., we have two separate judgments for type inference and type checking. To check a typing judgment we have two possibilities:
1.
2.
The solver starts with a top-down approach and defers to the bottom-up approach if necessary. Equality checks are used for solving variables and by using additional solution rules. This approach is described in [Rab17a] in detail and is largely irrelevant for the purposes of this thesis, hence details are omitted. The details on implementing typing rules in Mmt are treated by example in Chapter 5.
Similarly to typing, we have two equality judgments: one for checking equality of two given terms and one for reducing a term to another one (simplification).
Our judgments are given in Figure 4.4.
|
|
|
|
Judgment
|
Intuition
|
|
|
|
|
|
is a well-formed context
|
|
|
|
|
|
is inhabitable (may occur on the right side of a typing judgment)
|
|
|
|
|
|
is a universe (inhabitable, and every with is inhabitable)
|
|
|
|
|
|
checks against inhabitable term .
|
|
|
|
|
|
type/kind of term is inferred to be
|
|
|
|
|
|
and are equal at type
|
|
|
|
|
|
computes to
|
|
|
|
|
|
is a subtype of
|
|
|
Figure 4.4: Judgments
For each of these rules, the solver assumes certain pre/postconditions to hold, which critically need to be preserved by the implemented rules. These are:
•
•
•
•
•
The rules given in Figure 4.5 capture the intended semantics of the judgments above and can be assumed to hold for any type system implemented in Mmt.
The upper row contains the rules for contexts. Note that even though we allow the type of a variable to be omitted (which will be helpful for records later), that is only allowed if a definiens is present. ( must be inferable from or otherwise known from the environment.)
The second row contains the rules for looking up the type and definition of variable.
The third row contains the bidirectionality rules, which algorithmically are the default rules that are applied when no type (resp. equality) checking rules are available: switch to type inference (resp. computation) and compare inferred and expected type (resp. the results).
The last row deals with universes and inhabitability.
4.3Typing Rules and LF
LF [HHP93a] is a logical framework based on the dependently-typed lambda calculus .
The grammar is given in Figure 4.6. The only deviation here is that we allow optional definitions in contexts, to make them syntactically equivalent to Mmt contexts (see Remark 4.1). LF specifically as implemented in Mmt is covered in more detail in [Rab17a]; the specific rules presented here are adapted from there.
The grammar in Figure 4.6 as well as the various grammars presented in Part II represent object-level languages independent of the Mmt language. If implemented within Mmt, it should not be seen as extending the Mmt grammar from Section 4.1.1 rather than being embedded within it; for example, the well-formed expression according to the LF grammar would be represented in OMDoc/Mmt as the well-formed expression according to the Mmt grammar.
Note that the grammar for contexts aligns perfectly with the grammar for Mmt contexts; hence we do not need to distinguish between the two apart from the well-formedness of the term components of the variables therein.
The universe rules of the framework are given in Figure 4.7 and are to be read in conjunction with the general rules in Figure 4.5.
The specific rules for the dependent function types in LF are given in Figure 4.8. Note, that even though LF has precisely two universes and , we still formulate the rules parametric in a generic universe , to allow for flexible extending the number of universes later (see Chapter 6, particularly Section 6.4).
We consider an abbreviation for .
We also write for the usual capture-avoiding substitution of for in .
We can now show that the usual variance rule for function types and the -rule are derivable. Even though plain LF has no notion of subtyping (in fact, every term has a unique type), extensions of LF may introduce subtyping principles, in which case this rule becomes important:
Proof.
1.
Assume , . It suffices to show . By Figure 4.8 we can conclude this from . Since we have and consequently , so the claim follows by .
2.
By the equality rule, we can show that given we have , which is precisely the conclusion of the computation rule. Moreover, we can show that every well-typed term has a principal type in the sense that (i) and (ii) whenever , then also . The principal type is exactly the one inferred by our rules (see Theorem 8.1). This is easily proven by induction on the grammar; however, as a result this property does not necessarily hold in the presence of other rules.
4.3.1Judgments-as-Types
The lambda calculus described above makes LF a functioning logical framework, i.e. a language to specify the syntax and proof theory of various logics, type theories and related systems. This is achieved by using the
Judgments-as-Types methodology, in which (as the name suggests) we assign types to the judgments of a given logic. We can interpret these types as the types of proofs that the judgment holds.
4.3.2Higher-Order Abstract Syntax
In this thesis we use the same notation for application of LF functions f to arguments as for the Mmt primitive application of a term to a list of terms . This is to avoid cumbersome notations for LF-applications like . However, it should be noted that technically (and internally) an application of a function on the level of LF-expressions is internally represented as - the symbol provided by the LF-theory is applied (in the sense of an OMDoc/Mmt-application) to the arguments and . In a naive implementation, this means that the head of the term is not in fact the symbol , but instead the symbol .
Furthermore, if we use LF to formalize another -calculus , we will need to provide constants for the - and apply-operators of . This naively means, that we need to reimplement many mechanisms which are already present in LF. Fortunately, we can use higher-order abstract syntax to have our new symbols inherit their core behaviors from the corresponding symbols in .
All of this makes it quite convenient to formalize type systems in LF. Internally, however, it is rather inconvenient to handle even simple function applications in , because of the nesting of -symbols on the various meta-levels involved.
For that reason, Mmt offers functionality that allows to signify symbols belonging to a higher-order abstract syntax, and abstract them away in settings where we would rather have the term look like than – for example when implementing rules.
4.4Mmt/LF Surface Syntax
By and large, I will show relevant examples in Mmt surface syntax directly whenever it is informative to do so. In this section I will consequently briefly introduce the structural syntax for Mmt and the relevant notations for symbols provided by LF. An in-depth tutorial on using the Mmt surface language to formalize mathematical content is available online.
Especially noteworthy is Mmt’s usage of highly non-standard delimiters, namely higher unicode symbols. This is in order to allow for all standard delimiters used by other systems to be used in notations when implementing the foundations of these. A structural environment is delimited according to the level on which it is implemented (see Figure 4.2): Modules are delimited with the symbol , declarations with and objects with . The colors correspond to the ones used in the available Mmt IDEs (jEdit and IntelliJ IDEA).
A theory named with meta-theory is given with the syntax theory T : M = . If no namespace is provided, Mmt will either take one provided by the meta information of the containing archive, or use a default namespace. A local namespace can be provided beforehand using the namespace command. Using the latter, the following will establish an empty theory with full URI :
The theory providing LF has URI ; however, Mmt provides the default CURIE abbreviation for its namespace - hence to create a new theory with LF as meta-theory, we can write theory T : ur:?LF = .
A constant is declared by giving its name, followed by its components separated by the object delimiter in arbitrary order. A component is either a type (starting with ), a definiens (starting with ) or a notation (starting with ), and is delimited with the declaration delimiter – e.g. a constant with type and definiens can be given either as c : T = t or c = t : T . Includes are given with include ?T
A notation is provided as a sequence of tokens and argument markers followed by a precedence. Argument markers are either a number literal (denoting the th argument of the constant), or denoting a variable to be bound by the constant. If is followed by a , the system expects the variables provided in an application to be typed, infering their types if none are provided by a user. If an argument marker is followed by a token followed by ellipses , the system recognizes that a sequence of arguments is expected, the elements of which are delimited by . Precedences are given as for some (positive or negative) integer – the higher the precedence, the stronger the notation binds. We will examine the notations provided by LF as an example:
Dependent function type are written as {x:A,y:B}C – a notational practice inspired by the Twelf system. Consequently, the notation for the symbol representing dependent function types has two argument markers: The first one being a comma-separated list of typed variables (represented as ) and the second one being a regular argument. Consequently, the theory declares as Pi # { V1T,...} 2 prec −10000. It is given a deliberately extremely low precedence, since dependent function types most commonly occur on the outside of a term. Analogously, lambda is given the notation [ V1T,...] 2 prec −10000.
Simple function types have the notation # 1...prec −9990. Finally, as usual in lambda calculi, function application has the notation # 1%w...prec −10, where represents arbitrary whitespace.
The syntax for views is rather analogous to theories. As a module, it is delimited with the module delimiter . A view named with domain and codomain is given via view v : ?T1 −> ?T2 = . Assignments are considered declarations and use as its symbol; i.e. an assignment is given as c=t.
For any with :
Formation:
Introduction:
Elimination:
Type Checking:
Equality:
Computation:
Figure 4.8: Rules for Dependent Function Types
Part II
Modular Design of Logical Frameworks
One crucial aspect of connecting libraries of mathematical knowledge to a universal framework – whether they come from theorem provers, computer algebra systems, databases or other systems – is to specify the ontological primitives of the system within the framework. Correspondingly, sufficiently expressive logical frameworks are needed to specify all the features such a system might offer.
A logical framework like LF [HHP93b], Dedukti [BCH12], or -Prolog [MN86] tends to admit very elegant definitions for a certain class of logics (such as first-order or higher-order logic, modal logics or classical type theories), but definitions can get awkward quickly if logics fall outside that fragment.
This often boils down to the question of shallow vs. deep encodings. The former represents a logic feature (e.g., subtyping) in terms of a corresponding framework feature, whereas the latter applies a logic encoding to remove the feature (e.g., encode subtyping in a logical framework without subtyping by using a subtyping predicate and coercion functions). Deep encodings have two disadvantages:
1.
2.
Even if we ignore the proof theory (and thus the use of decision procedures) entirely, PVS (which we discuss more in-depth and integrate in Chapter 10) is particularly challenging in this regard, and hence serves as a good example for the challenges involved:
•
•
•
•
•
Florian Rabe has extensively investigated definitions of PVS in logical frameworks, going back more than 10 years when a first (unpublished) attempt to define PVS in LF was made by Schürmann as part of the Logosphere project [Pfe+03]. In the end, all of the above-mentioned difficulties pointed in the same direction: the logical framework must adapt to the complexity of PVS– any attempt to adapt PVS to an existing logical framework (by designing an appropriate deep encoding) is likely to be doomed. This negative result is in itself a notable contribution of [Koh+17c], where the PVS import described in Chapter 10 was first published. Since publication, we have found this to also hold for similarly complex object logics such as Coq.
Hence we need logical frameworks with advanced features. However, not all additional features should be active and available simultaneously all the time – the additional inference rules, even if in conjunction logically sound, can cause problems such as slowing down type checking, reserving notations, making the type system unnecessarily complex and potentially destroying adequacy of a library translation. Especially the first can happen easily in the presence of a critical pair of typing rules – two rules concluding the same judgement, but from different (and potentially expensive to check) premises. An example for such a critical pair on the meta-level is the two fundamental strategies in a bidirectional type checking algorithm (see Section 4.2.1).
What we actually need in practice is therefore a modular meta logical framework with a library of optional features that can be included on demand.
This library can be seen as an analog for LATIN (see Section 3.1) for logical frameworks. Where LATIN resulted in a modular library for logics using a fixed logical framework (namely LF), what we need to go beyond the “simple” logics in LATIN is a similarly modular library of logical frameworks, written in an appropriate meta-framework.
This is more difficult than it seems in that the rules for each feature must be implemented in such a way that they are orthogonal – they should be compatible (if possible) with each other and be minimally dependent on other features. A natural starting point of such a framework is the set of orthogonal features of Martin-Löf type theory [ML94], which are covered in Chapters 5 and 6. One of these – dependent function types – is already implemented by LF and described in Section 4.3.
Various extensions of LF have been proposed and designed before; [Pfe93] presents an extension of LF with refinement types (and intersection types, which we will cover in Section 7.3), [Sto+17] adds additional union types (essentially equivalent to coproducts, see Section 6.1). The grammatical framework GF [Ran04] is based on an extension of LF by record types.
Apart from the latter, all the mentioned extensions lack an implementation, and all of them have been designed with the additional feature as a primitive – in other words, the rules are intrinsically non-compositional and consequently not suited for a modular approach. The advantage of the primitive approach is that it allows for tightly controlling the interactions of different primitive typing features. This makes it relatively easy to ensure some desirable aspects of the typing system in the presence of several features at once, such as good performance or decidability. In fact, [Pfe93] makes decidability one of its central results. Our modular approach on the other hand makes it considerably more difficult to verify these kinds of properties. However, adding e.g. predicate subtyping to a logical framework – as is necessary for formalizing PVS for example (see Chapter 10) – renders the type system immediately undecidable anyway. This also holds for many other features that increase the expressivity of a logical framework, such as the model types presented in Chapter 8. Since expressivity is our primary concern, we consider losing decidability less of a problem in the context of this thesis. Similarly, in a tradeoff between modularity/expressivity and performance, we prioritize the former.
Conveniently, the modular implementation of the type checking component of Mmt, and the abstractions provided in the Mmt API, result in a very small difference between the theoretical design of a logical framework and its implementation in Mmt. In fact, the set of formal rules as developed on paper corresponds closely to the set of implemented classes in Scala.
An example for such a feature is the naive implementation of declared subtyping in Section 7.2. In general, we try to avoid such implementations in this thesis.
In this part, I will present various extensions of LF. In doing so, I will explain in detail how to implement new language features in Mmt. For that reason, we will start with a relatively simple feature – namely -types in Chapter 5 – as an introduction to the relevant classes of the Mmt API. Chapter 6 covers additional simple typing features (primarily those of Martin-Löf type theory), culminating in a logical framework based on homotopy type theory [Uni13] as a case study in Section 6.5. Our approach to implementing logical frameworks in Mmt is briefly described in [MR19], but essentially previously undocumented and hence covered in greater detail.
Continuing with more complicated features, Chapter 7 covers subtyping mechanisms in Mmt, and Chapter 8 covers our implementation of record and model types in detail.
All the rule systems presented in this part follow a general pattern for typing rules presented in Remark 4.5. Also, note Remark 4.4 on how to read our rules algorithmically. The Mmt API provides a dedicated class interface for each kind of rule – Figure 4.9 gives an overview of those covered in this part.
|
General Aspects
|
|
|
Mmt Judgments
|
|
|
Symbol References
|
|
|
Solver Judgments and Continuations
|
|
|
|
|
|
Typing Rules
|
|
|
Type Inference Rules
|
|
|
Type Checking Rules
|
|
|
Subtyping Rules
|
|
|
Universe Rules
|
|
|
|
|
|
Equality Rules
|
|
|
Type Based Equality Rules
|
|
|
Term Head Based Equality Rules
|
|
|
Irrelevance Rules
|
|
|
Computation Rules
|
|
|
|
|
|
Other Features
|
|
|
Generic Literals
|
|
|
Structural Features
|
|
|
Rule Generators / Change Listeners
|
Figure 4.9: Table of Mmt API Classes for Solver Rules
Most inference rules in Chapters 5 and 6 are taken from [Uni13] with minor adaptations to minimize dependencies on other typing features and be consistent in their presentation with the rest of this thesis. Where multiple design options exist, these are discussed explicitly – notably, in that case we do not decide on a specific rule system, but rather implement all of them as separate theories extending the same core rules, allowing to pick the most adequate implementation for a given logic formalization while reusing the same symbols across logics for the required features.
Chapter 5
Implementing Rules in Mmt (e.g. -Types)
In this chapter we will go over the implementation of -types in Mmt in detail, as a relatively simple example on how to extend the Mmt solver with rules in a modular fashion. The main contribution of this chapter is the adaption of the typing rules governing -types into the Mmt framework and their implementation, as well as a detailed explanation of our methodology for constructiong a modular meta logical framework.
5.1The Rules for -Types
-types are the dependent variant of cartesian products . The type is populated by pairs with and , hence we can consider as an abbreviation for , where does not occur in . The elimination forms are the two projections and . -types are conveniently simple, since they fall nicely into the pattern from Remark 4.5 and do not interact with -types in any significant way.
Since -types arise naturally as the dependent variant of Cartesian products, their history is difficult to reconstruct. To the best of my knowledge, they, along with most of the features in the subsequent chapter, were originally introduced as a consequence of the Curry-Howard correspondence (as e.g. in [ML94]), where the simple products correspond to conjunctions and dependent -types correspond to the existential quantifier .
The grammar for -types is given in Figure 5.1.
The rules are correspondingly intuitive and given in Figure 5.2 (adapted from [Uni13]).
Proof.Analogous to Theorem 4.1
Before we look at the implementation, a couple of things should be noted:
1.
2.
3.
5.2Implementing Rule Systems in Mmt
5.2.1Mmt Symbols in Scala
Before implementing the rules themselves, we create an Mmt theory that contains the symbols we need, so that we can assign them proper notations determining their syntactic usage and refer to them in the implementations of the rules. In the case of -types, this theory contains a symbol for the type constructor , the introduction form and the two elimination forms . For convenience we add an additional symbol for simple products . The resulting theory is given in Listing 5.1.
Note that we specified the notations of , and all to be flexary – hence our rule will have to deconstruct a type into the actual type , and analogously a tuple into the actual term .
For convenience, we can implement helper objects in Scala, that provide apply and unapply methods to easily construct – and pattern match against – applications of our symbols. These can not only take care of the flexary notations, but also take care of being an abbreviation, which makes implementing our rules easier and more uniform.
5.2.2Solver Judgments
The solver checks a judgment by collecting all rules included in the context that correspond to the type of the judgment (an extension of the class Judgment), checking which of them are applicable and trying them in order of priority. These Judgments are:
•
The judgment is checked by iteratively simplifying both terms using ComputationRules (see Section 5.2.6) until they are syntactically equal or an EqualityRule (see Section 5.2.5) is applicable.
•
•
•
To implement our rules, the Mmt API provides the mentioned abstract classes for the different rule types. All of their extensions need to implement an apply-method with a particular signature. A Solver is passed on to the rule to allow for recursive checking and inference calls.
The most important methods a Solver provides for a rule are:
•
•
•
•
•
5.2.3Inference Rules
Formation, introduction and elimination rules are all trivial extensions of the class InferenceRule. They take as class argument the head symbol of the terms to which they apply (and the typing symbol used for the typing judgments) and its apply-method has the following signature:
where tm is the term whose type is to be inferred, and covered is a boolean flag that tells the rule whether the term tm has already been checked to be well-typed, and hence that the preconditions (see Section 4.2.1) are satisfied.
The implicit argument stack contains the context in which the type of tm is to be inferred. history is an object that holds textual information on the current state of the solver – if a check fails, the history is presented to the user as feedback.
An inference rule with head is considered applicable to a term, if the head of the term is . Additionally, a rule can override a method alternativeHeads:List[GlobalName] if it should be applicable to other heads as well, as in our case with and (see Example 5.3).
5.2.4Checking Rules
Similarly to inference rules, TypingRules (which trivially extend CheckingRule) take the head symbol of the type to which they apply as argument. They too have an overridable method alternativeHeads:List[GlobalName] if multiple head symbols are covered. Additionally, checking rules can shadow other rules (by overriding the method shadowedRules:List[Rule], in which case the shadowed ones are deactivated in the presence of the new rule. Furthermore, checking rules can be assigned a priority : Int with default value 0 to control in which order the solver attempts multiple applicable rules. The signature of their apply-method that needs to be implemented is
Alternatively to returning a simple Some(Boolean) value, checking rules can also:
1.
2.
3.
5.2.5Equality Rules
The Mmt API provides three classes for equality rules: TypeBasedEqualityRule, TermBasedEqualityRule and TermHeadBasedEqualityRule.
•
They take as class parameters the head symbol of the governing type, as well as a (possibly empty) list of application-symbols, in case that the type constructor is applied using a higher-order abstract syntax. This can be used to implement equality rules for e.g. symbols from a logic or type theory which is itself implemented in a logical framework.
Additionally, an instance of this class has to implement an applicableToTerm-method. This is convenient in case where the rule requires the two terms to have a specific form.
The signatures of the methods to implement are:
The applicableToTerm-method will be called on both terms and the rules is considered applicable if either returns true.
The apply should return Some(true) or Some(false) if the equality of the two terms tm1 and tm2 is provable or disprovable, and None if the solver should proceed trying other equality rules.
•
The applicable-method should fail quickly; preferentially it should only check whether the terms tm1 and tm2 have a specific syntactic form.
The apply-method only takes a CheckingCallback, which is a superclass of Solver with slightly limited functionality.
•
5.2.6Computation Rules
Computation rules implement the class ComputationRule, which takes as class parameter the head symbol of the term to decide applicability. This is only a default implementation, though – the governing method def applicable(tm : Term): Boolean can be overridden. The apply-method has the following signature:
It returns an object of type Simplifiability that instructs the solver (or other CheckingCallback instance) on how to recurse into a term. The latter has by and large three possible instances:
1.
2.
3.
The solver can use the information returned by a ComputationRule to strategically recurse only into those subterms that might cause a rule to become applicable, without unnecessarily simplifying subexpressions or expanding definitions.
5.2.7Subtyping Rules
Finally, to implement subtyping rules Mmt offers a generic class SubtypingRule, and conveniently a more specific class VarianceRule for the case where we want to declare an operator to be covariant or contravariant in its arguments. The former needs to implement an applicable(tp1 : Term, tp2 : Term)-method, the latter takes a head symbol as class argument that determines the applicability of the rule. In both cases, the apply-method has the signature
After implementing the rules in Scala, we can import them into an Mmt theory. Including the latter into any theory will then activate those rules. It makes sense to declare the symbols and rules in separate theories, so we can reuse the same symbols with different sets of typing rules, as in Listing 5.8. Ultimately, we implement four theories in total: for the symbols (), the rules (), a theory that combines symbols and rules in the context of the basic typing rules (see Figure 4.7) from LF (), and finally one that adds symbols and rules on top of the full LF theory with dependent function types (). We will roughly follow this naming convention throught this part; the various theories for e.g. the symbols are disambiguated by the namespaces (in this case ).
The statement in the first line of Listing 5.8 introduces an abbreviation for the namespace , which by virtue of the -scheme determines the fully qualified class path of the scala objects referenced by the subsequently declared rule constants.
5.3Using -Types
The theory in Listing 5.9 from the Math-in-the-Middle library serves as an example; it uses -types to implement the product of two vector spaces, by defining the corresponding operations on the product space – since the latter is a natural occurence of Cartesian products in mathematics, -types are naturally ideal for formalizing products of spaces (analogous e.g. product topologies, categories etc.). In fact, thanks to -types,the definitions for the universes, operations, units and inverses here conforms quite naturally to the usual informal presentation of product spaces.
For any with :
Formation:
Introduction:
Elimination:
Type Checking:
Equality:
Computation:
Figure 5.2: Rules for -Types
Chapter 6
LFX
[LFX] is an Mmt archive that contains various features as extensions of LF. Two such extensions are already part of the archive [OMU], namely PLF (see Remark 4.6) and LFS [HKR14], that adds flexary operators and sequence arguments.
Many of the features in this chapter are primitives in homotopy type theory, and are hence treated in some detail in [Uni13]. The contribution of this chapter consists, as the previous chapter, in adapting the rules for the typing features covered here to the Mmt framework and their implementation. Together and correspondingly modularly implemented, these features yield a flexible, modular meta logical framework following the LATIN approach.
6.1Coproducts
Coproducts can be seen as disjoint union types – their introduction form is a simple embedding, the elimination a case distinction on the constituent types and . In particular, coproducts give us a relatively simply implementable mechanism for pattern matching.
Under propositions-as-types, coproducts are the type-level correspondants to logical disjunction. Additionally, they arise rather naturally as the (cateogory theoretical) dual notion to simple Cartesian products.
To be more precise:
•
•
•
The grammar for coproducts is given in Figure 6.1
The basic rule system is given in Figure 6.2, but can be extended for a more desirable behavior in presence of subtyping.
In a categorial setting, coproducts are dual to certesian products as covered in Chapter 5. As a result, the roles of introduction and elimination forms in our rule pattern are somewhat reversed. Consequently, there are a couple of things to note about our rules:
•
•
•
•
The crucial premise here is the second one, since to evaluate the -expression, we will need to infer the type of . Hence this typing rule would in practice reduce to checking whether the inferred type of is a subtype of , something the solver checks as a default anyway.
•
•
It is thus debatable whether “equal for any particular introduction form” should imply “equal everywhere”. If we answer this question positively we imply axiom K [HS02], which is equivalent to term irrelevance for equality types and hence incompatible with e.g. HoTT (see Section 6.5) and similar constructive systems. Hence, if we want to add an equality rule to preserve extensionality, we should do so in a separate theory and exclude it when formalizing constructive logics and type theories.
6.1.1Subtyping Behavior of Coproducts
We have previously used the type checking rules as a justification for derivable subtyping rules. Since a type checking rule for arbitrary elements of does not exist (in a meaningful way), we can instead introduce a subtyping rule and use that to derive type checking rules for the introductory forms. The obvious guiding criterion to use is that any pattern match on needs to be applicable to any for . This implies the following covariance rule:
from which we can derive the following typing rules:
This is especially useful in the presence of an empty type (see Section 6.2), where now type checks against any (analogously for ). However, we also need to add an additional equality rule then, since all left injections should be equal (at some -type). Hence:
6.1.2Implementation
Given the rules in Figure 6.2 and the examples in Chapter 5, an implementation of Coproducts is rather straight-forward.
Listing 6.1 and Listing 6.2 show excerpts of the associated Mmt theory and a toy example for testing the implementation. Notably, both and are implemented with flexary notations; a helper object (similar to -types, see Chapter Chapter 5) takes care of deconstructing expressions with multiple arguments into binary applications of the symbol.
Notably, coproducts are not very useful in and of themselves; however, in conjunction with a unit type they are sufficient to construct finite types (see Section 6.2), and are used to construct -types (see Section 6.3).
6.2Finite Types
Finite types are types with a fixed, finite number of elements. Their predetermined number of elements can be exploited using case distinction. Their usefulness is immediately obvious when trying to formalize e.g. finite groups and functions between them, but they are also ubiquitous in e.g. object-oriented programming languages. Naturally, it is sufficient to have for each natural number one type with elements, since all finite types with the same number of elements are isomorphic. Therefore we will focus on this approach, since it conveniently introduces names for the members of finite types and spares us the trouble of having to label them.
Starting with the empty type , we face the question how to formally declare that this type has no elements. Since we can always declare a new constant we need to make sure that the existence of this constant leads to a contradiction. We can do so by allowing to construct a term of any type given an element of , which (using Curry-Howard or judgments-as-types) corresponds to the principle ex falso quodlibet. There are three ways to go about this:
also called enumeration types, however, this usually refers to (a priori mutually disjoint) types with finitely many uniquely named elements.
1.
2.
3.
The obvious advantage of the second approach is that it allows using like an actual typed function. The disadvantage is that using this approach requires function types to be present, hence reducing modularity, and the advantage is negligable.
The third approach has the advantage that it obviates the need for an elimination form completely – a postulated element already gives us an element of every other type, namely itself.
Given an additional singleton type with a single element , we can use the coproducts implemented in Section 6.1 to construct the remaining finite types. This way, we can use the elimination form for coproducts to pattern match an element of a finite type, obviating the need for a dedicated elimination form. There are two ways to do this:
1.
2.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
and is the same expression at all numerical types. In particular, we can easily define the successor function as .
Conveniently, defining to be a subtype of any other type allows for implementing both variants.
In the presence of function types, we can also define as , knowing that the only possible inhabitant of this type is the function . However, even using this definition, we still have to provide a rule for the solver to be able to exploit this knowledge (and to make sure that is the identity).
All of this leaves us with several options listed in Figure 6.3 and the basic rules in Figure 6.4.
Of course, constructing enumeration types and their elements by nesting -types and injections is simple to formally specify and implement, but inconvenient to use in practice. Furthermore, while it is possible to build up enumeration types using even in the absence of coproducts by adapting their rules, the most general and user-friendly way to implement finite types is via a primitive type constructor on actual integers.
We can do so using a type of number literals, which we discuss further in Section 6.2.1:
We implement a type constructor for the type , and analogously a constructor for . In this case, it is desirable that is a valid type even if is a variable or otherwise undetermined and checks against type iff . If and are not definite number literals, this implies proving a judgment , which requires corresponding proof rules for the ordering on natural numbers and a way for the user (and the solver) to construct (and find) such proofs.
If we want to consider enumeration types as subtypes of each other, the argument in becomes unnecessary, so we can write instead.
Figure 6.5 gives a set of rules for these -types, where represents the (or any variant of, in the case of subtyping) defined finite type corresponding to the (definite) number literal , and represents an element of such a type (again, for a definite number ). Which of the optional rules to implement depends on which of the implementation approaches discussed above we choose.
To summarize: Finite types give us various ways of implementing their different aspects, depending on which additional typing features are available in any context and how we want them to behave with respect to subtyping. Note however, that implementing all constructors as primitives still allows us to reuse the symbols already implemented for other typing features: A primitive elimination form for finite types can reuse the -symbol from the theory for coproducts, and we can reuse the -symbol to construct higher finite types even in the absence of the rules governing coproducts. Even the rules governing these symbols can be reused with minimal adaptation (to restrict the types that are valid arguments to finite types).
This allows for developing library content with minimal dependencies, allowing for adding new features (e.g. coproducts or function types) as needed without reimplementing content that was developed without these features. The additional features only provide new definitions for the already implemented formalizations without changing their semantics significantly. Consequently, we will omit the rules for the constructs already covered in the previous sections in the basic rules listed in Figure 6.4.
6.2.1Generic Literals in Mmt
To implement and , we need to be able to explicitly use numbers and have them be syntactically valid and semantically meaningful Mmt terms – i.e. we want them to be literals. The Mmt API offers a class RealizedType for generic literals, which combine a syntactic type (an inhabitable Mmt term) with a SemanticType. A SemanticType represents an actual Scala class holding the values of our literals, as well as a lexer used to parse them in surface syntax.
Additionally, the Mmt API already implements SemanticTypes for the most prevalent literals and their corresponding Scala implementations, namely BigInt (unrestricted integers), String, Double (floating point numbers), Boolean etc. In our specific case, we can use StandardNat extends SemanticType, which uses BigInt values restricted to positive numbers.
Mmt’s library [OMU] also already has a theory with a type that we want to use as a syntactic type. To couple the two, we import a rule in an Mmt theory, which we either implement in Scala (using the class RealizedType), or even more conveniently by import the parametric rule Realize with the name of the SemanticType and the syntactic type as parameters:
Hence, by importing the above theory we can use integer literals which will be assigned the principal type .
6.2.2Implementation and Irrelevance Rules
One noteworthy aspect of the rules in Figure 6.4 is that the equality rule tells us that all terms of a specific type are equal – in other words, the type has (at most, i.e. in this case) exactly one element. While mathematically both of these statements are logically equivalent, they are intrinsically different from the point of view of an implementation.
In an implementation, to leverage the first statement we need two syntactically distinct terms that can then be shown to be equal. Hence this rule will only ever become relevant in presence of two distinct terms of the same type . The second statement however tells us that whenever we need any term of type , e.g. to solve a variable of type , there is exactly one element that we can use.
There is a dedicated rule class for these situations, namely TypeBasedSolutionRules. These not only extend TypeBasedEqualityRules, but also tell the system that which term of the given type is used is irrelevant, and more specifically, how a variable of this type should be solved. This is particularly relevant in the presence of judgments-as-types and proof arguments, where usually the specific term (i.e. proof) of a given judgment type is irrelevant, as long as there is any such term (this is called proof irrelevance), in which case the solution rule can activate the prover.
Listing 6.4 shows the Mmt theories associated with all the above options for finite types. Note their modular development, offering theories that mix in basic LF, or coproducts, or both, with or without subtyping. Figure 6.6 shows the corresponding development graph with the symbol theories at the bottom.
Notably, finite types allow us to implement finite functions in an exploitably computational manner. As an example, Listing 6.5 shows a formalization of the finite group and its group operation in such a manner, that the solver manages to compute from the definition of the operation. While the definition of is syntactically ugly, one could imagine using a structural feature (see Section 6.3) specifically to introduce finite functions.
6.3-Types
-Types were introduced in [ML94] to represent wellorderings, but were shown to be able to represent many other inductively defined sets in Martin-Löf style type theories as well (see [Dyb97]). The central idea is to define an inductive type from the number of constructors of the type and their arities with respect to the type that is being defined; the introduction and elimination forms then assure that the resulting type represents an initial algebra.
Ignoring the category theory involved, how to represent inductive types as -types is best explained by example:
- note that the theory development used in the actual implementation is only a fragment of the more modular version described here.
As introduction form for a -type , we have a supremum-operator , where tells us the constructor case, is a variable that represents the inductive parameters needed, and represents the arguments for the constructor. How this works is again best understood by example:
Elimination of -Types is cumbersome and technical, so it is worth going into some detail. To eliminate an element of a type , we want to define a function out of with target type (for ) via well-founded recursion. For every constructor case , we have an arity of , so we would have to define on and the many (recursive) arguments of type . The latter can be encoded (or thought of) as a function . Additionally, we need to be able to use the recursive values of the very function we are defining on the recursive arguments encoded in . These we can similarly think of encoded as a function
Hence, to be able to define we need an element a way to obtain for any for the recursive arguments, and a way to obtain for any . The easiest way to do so is to have the elimination constructor bind variables for these, some of them representing (dependent) functions. This requires function types, of course. In the absence of function types, the rules governing them can be added without making the symbols associated (lambda-abstraction, function type constructors etc.) available to the user. Alternatively, one could implement dedicated syntactic constructs that basically mirror the application of functions in the particular context of recursive definitions on -types, which is even more cumbersome, but theoretically straight-forward. I will hence for simplicities sake assume function types to be present in the remainder of this Section.
|
|
|
|
|
|
|
|
The resulting grammar is given in Figure 6.7, the rules are given in Figure 6.8. Again there are several things to note:
•
•
•
6.3.1Implementation
From an implementation perspective, -types are conveniently simple and fall neatly into our pattern of rules. Consequently, implementing them in Mmt is straight-forward; the corresponding Mmt-theory is presented in Listing 6.6.
From a user perspective however, -types are incredibly inconvenient and unintuitive, counter to our goal of being as close to mathematical practice as possible. Listing 6.7 shows as an example the natural numbers with inductively defined addition on them.
6.3.2Structural Features
We can remedy this inconvenience by providing a structural feature that offers a more convenient and intuitive syntax and elaborates into -types, giving users a way to specify inductive types without having to use the cumbersome syntax offered by -types – or having to know about them at all. The goal is to formalize natural numbers more akin to this:
A structural feature is an extension of the class StructuralFeature. Firstly, it instructs the parser how to parse the header of an instance of this feature (e.g. ). For this, the structural feature has to provide a notation. The header is followed by an optional body of a theory (e.g. containing the declarations , and ). The parser wraps any application of the header notation into an object of class DerivedDeclaration, holding the components provided in the header and the optional body.
Secondly, after parsing, this DerivedDeclaration is passed on to the StructuralFeature, which returns an Elaboration, holding a list of Mmt declarations computed from the DerivedDeclaration. The details on implementing derived declarations and structural features are sketched in [Ian17] and thus omitted here.
For inductive types, we want two structural features: One that elaborates into a -Type and its constructors, and one for the elimination form. The keywords for these features are set as induct and def respectively, which allows us to implement natural numbers and addition in surface syntax as in Listing 6.8.
All declarations in an or -environment are bundled into the body of a theory, which is itself wrapped into a DerivedDeclaration . This declaration is then passed on to the StructuralFeature’s elaborate-method, which in the case of computes from them the appropriate -type (e.g. for ) and the constructors (e.g. and ), and in the case of the corresponding function defined by a -expression. We can pass additional parameters to the structural feature in the header of an or environment, to allow for e.g. polymorphic -Types or inductive functions with arity (as in ), as shown with lists and binary trees in Listing 6.9.
6.4Cumulative Universe Hierarchies
Plain LF offers two universes and . With respect to their ontological status, they can be thought of as analogous to the distinction between sets and proper classes. However, often the two universes are somewhat restrictive – PLF is already an extension of this two-tiered hierarchy, but even the shallow polymorphism enabled by it is often not enough, e.g. when wanting to quantify over all groups (each of which has a base type), or sets (for some correspondance between sets and types), or when formalizing categories while trying to avoid a deep embedding.
In those situations, it can be more convenient to have
infinitely many universes for each . By declaring and whenever , we get an infinite cumulative hierarchy of universes analogous (in a set-theoretic model) to higher levels of the Von-Neumann hierarchy indexed by large cardinals.
This is the approach taken by homotopy type theory [Uni13], Mizar [Miz] via Grothendieck universes, and most notably Coq [Tea03], where the precise universe in which a declaration lives is unspecified by the user and computed by the system by solving appropriate constraints on the full current context (floating universes).
The basic rules are straight-forward and given in Figure 6.9, and as with enumeration types (Section 6.2), we use number literals and postulate some (potentially judgments-as-types based) judgment .
To be “backwards compatible” with everything implemented in LF alone, we can redefine and . Even though does not hold in LF, this additional subtyping judgment does not impact plain LF content. However, in order for -types to be usable for types living in higher universes, we need to slightly modify the formation rule for :
Note, that for , this subsumes the original rule. Since we can declare our new formation rule to shadow the old one, this does not break modularity. In addition, we augment Definition 4.1 by new cases:
To be precise: Any judgment that holds in LF still holds in this new logical framework, but not the other way around.
These kinds of formalizations are enabled by using e.g. record types with -valued fields, see Chapter 8
According to folklore, all mathematics can be done with at most 7th-order universes, but this number is seemingly arbitrary and in practice it is just as easy to drop the restriction to a fixed finite number of universes entirely.
6.4.1Implementation and Universe Rules
All the rules are again straight-forward, but here we encounter a universe rule for the first time. As with the other rules, we need to implement an apply method for them, the signature of which is rather simple:
and returns true if the term tm is declared to be a universe by this rule.
The corresponding theories for the symbols and rules are given in Listing 6.11. Notably, the theory TypedHierarchy which is to serve as a “standalone” theory of a cumulative type hierarchy without any typing features, needs to import several fundamental Mmt theories that validate notions like typing, notations, module expressions etc. in the first place, as well as the theories containing the symbols for and for compatibility with plain LF theories. Listing 6.12 shows a small example theory using a cumulative hierarchy. Additionally, universes are used all over the Math-in-the-Middle archive, notably in the algebraic theories and in categories.
6.5A Logical Framework Based on Homotopy Type Theory
Homotopy Type Theory [Uni13] (HoTT) is a foundation of mathematics built upon a type system that we can now define as LF+Cumulative Universes+-Types+-Type+Finite Types+-Types. It is based entirely around Propositions-as-Types, as summarized in Figure 6.10 – more precisely, the “propositional” part of homotopy type theory is an intuitionistic higher-order logic: Our proof rules can be easily observed to correspond to the usual introduction and elimination rules of a natural deduction calculus for intuitionistic logic. To get to a classical setting, it suffices to add a polymorphic constant – which by Propositions-as-Types corresponds to the statement for all “propositions” .
Formalizing HoTT in a logical framework such as LF is prohibitively difficult; a previous formalization by Florian Rabe is available online and shows the limitations of such an attempt: Even -types can only be fully formalized in LF by adding simplification rules (see Remark 5.2) and -types are left out entirely. Furthermore, since HoTT is – like LF– based on a Martin-Löf type theory, a formalization within LF requires re-implementing that very type theory using a HOAS deep embedding, with all the associated drawbacks for working with and within the resulting formalization. This is contrasted by HoTT’s aim to be a foundation of mathematics alongside and orthogonal to other such frameworks. Consequently, it is much more adequate to lift an implementation of Homotopy Type Theory to the level of logical frameworks itself. Additionally, this makes HoTT an attractive case study for a modular logical framework.
Homotopy Type Theory is a framework under active investigation and development, and hence frequently subject to change and subtle shifts regarding formal details. The description here follows the presentation in [Uni13], which does not necessarily reflect the current state of the art.
Accordingly, the following definitions and theorems are all taken from the same source and described in much more detail there. They are only contained here for clarification. In particular, we omit all proofs.
6.5.1Identity Types
Notably, in the correpondences in Figure 6.10 we are yet missing (propositional) equalities. For these, we can add a simple equality type whose semantics is provided by the intended propositions-as-types correspondence.
However, HoTT is somewhat peculiar here, since it does not consider propositional types to be proof irrelevant - Equality of elements is considered a type with arbitrarily many distinct elements, and this notion of equality is distinct from the judgmental equality . In particular, the existence of a “proof” does not imply . The reverse implication holds trivially by the introduction form, for which we use reflexivity: For every , we have .
For elimination we use a mechanism called (in the context of HoTT) path induction: Given any and , we have , where for any we demand that and will declare that . This requires some deliberation:
The central idea is that given a proposition (or type) depending on , if we have a proof/element and a proof , then we should also have a proof/element (congruence of equality). This is what yields in the simple case where only depends on .
In homotopy type theory, this principle is generalized in that the type may depend not just on , but also on an element considered propositionally (but not necessarily judgmentally) equal to , as well as the proof for that equality. The postulated judgmental equality can then be interpreted as the statement that the family of types (for fixed and variable ) is inductively defined by the elements of the form , in the sense that any type family for and is determined by the cases of the form .
Note that this does not imply that the types (for fixed elements ) are themselves inductively defined via the elements – whenever and are not judgmentally equal, this type is not inhabited by a -term at all.
The rules for identitiy types are given in Figure 6.11. Note that if we wanted to identify propositional equality and judgmental equality , we could add a corresponding equality rule.
6.5.2Equivalences and Univalence
The principal idea behind homotopy type theory is to interpret propositional equality topologically: Given two “points” , the type is interpreted as the type of all continuous paths between and . This makes sense of the multitude of possible “proofs” of , since not all continuous paths between points are equal. Two such paths can be equivalent though, in the sense that there can be a continuous transformation from to - i.e. there can be a path - making a homotopy.
We can now use homotopies to define two types as equivalent in the category theoretical manner: A function is an equivalence (isomorphism) if it is invertible (up to homotopy), and two types are equivalent (isomorphic) if there is an equivalence between them:
The final step that Homotopy Type Theory takes is to declare function extensionality (on equivalences) and postulating the univalence axiom that declares equality of types itself an equivalence.
6.5.3Implementation
Implementing the rules for identity types as in Figure 6.11 is straight-forward. All concepts and axioms of Homotopy Type Theory beyond our previously covered typing features can conveniently be specified in MMT syntax directly, as in Listing 6.13.
For any with :
Formation:
Introduction:
Elimination:
Equality:
Computation (Optional):
Subtyping (Optional):
Figure 6.4: Basic Rules for Finite Types
Formation:
Introduction:
Elimination:
Type Checking (Optional):
Equality: Computation (Optional):
Subtyping (Optional):
Figure 6.5: Convenience Rules for Finite Types
Figure 6.6: A Modular Development Graph for Finite Types
|
|
|
|
contexts
|
|
|
|
|
variables and universes
|
|
|
|
|
-types
|
Figure 6.7: Grammar for Coproduct-Types
For any with :
Formation:
Introduction:
Elimination:
For :
Computation:
For , , and :
Figure 6.8: Rules for -Types
Universe Rule:
Formation:
Subtyping (Optional):
Figure 6.9: Rules for Universes
|
Higher-Order Logic
|
Homotopy Type Theory
|
||
|
|
|||
|
Constant symbols
|
|
constants
|
|
|
Function symbols
|
|
functions
|
|
|
Predicate symbols
|
|
functions
|
|
|
|
|||
|
Propositions
|
|
types
|
|
|
Conjunctions
|
|
Simple Products
|
|
|
Implications
|
|
Simple Function Types
|
|
|
Disjunctions
|
|
Coproducts
|
|
|
Negations
|
|
Function Types
|
|
|
Universal Quantifier
|
|
Dependent Function Types
|
|
|
Existential Quantifier
|
|
|
|
|
|
|||
|
Proofs for
|
Elements
|
Figure 6.10: Propositions as Types
For any with :
Formation:
Introduction:
Elimination:
Figure 6.11: Rules for Identity Types
Chapter 7
Subtyping
The previously discussed subtyping rules were almost exclusively concerned with variance behavior of type constructors, i.e. rules of the form if (depending on the variance) or . Naturally, in the absence of any additional subtyping rules, these variance rules ultimately reduce to equality rules, since the only way to prove (ignoring recursively calling variance rules) is to check . However, some systems allow for primitive subtyping principles of various forms, e.g. by declaring axiomatically for two primitive types or by introducing predicate subtypes. Systems with subtyping mechanism include e.g. PVS [ORS92], IMPS [FGT93] and – in a certain sense – Coq [Coq15] and Matita [Asp+06a], as we will discuss later. Variance rules are accordingly important for the composite types to behave as intended in the presence of primitive subtyping principles.
Notably, subtyping in general breaks several often desirable properties of a type system, such as terms having a unique type and (potentially) decidability. Consequently, many systems decide to not support any subtyping. While this allows for a convenient implementation and formal analysis of a system, it often leads to awkward formalizations of content which can be implemented very naturally with subtypes. For example, numerical types (natural numbers, integers, real numbers) are often desirable to behave as subtypes. Similarly, types for algebraic structures yield a very natural subtyping hierarchy (e.g. all groups are monoids).
In this chapter, I will discuss various approaches to implementing subtyping principles in Mmt, how and why they are not fully implementable in the system, and speculate on how to improve Mmt to better support subtyping mechanisms.
7.1Issues with Subtyping in Mmt
Mmt supports subtyping in the form of a binary subtyping judgment and rules returning these judgments as conclusion. Notably however, a binary subtyping judgment is insufficient to exploit all deducable subtyping judgments without additional treatment or huge increases in computational cost. A simple example is transitivity:
This example alone is sufficient to demonstrate that merely checking binary subtyping judgments is not sufficient for covering subtyping mechanisms found in other systems.
One way this can be resolved is by keeping the full subtyping lattice for the current context in memory, and dynamically expanding it whenever the context is extended by additional types. Additionally, we can model subtyping premises as constraints (i.e. lower and upper bounds in the subtyping lattice), and introduce appropriate constraints when encountering unsolved type variables. These can then be solved in a manner similar to the method proposed in [KP93]. Notably, to be able to solve these constraints the full subtyping lattice still needs to be known. The feasibility, potential cost and benefits of this approach will need to be explored.
Additional problems arise whenever it becomes necessary to coerce a term to a refinement of its principal type:
This problem can in principle be solved by introducing an object-level typing-predicate with a rule of the form
By allowing arbitrary terms for and and quantification on the outside, this corresponds to term declarations [SS89]. Again, how to implement this efficiently and whether doing so is an effective solution remains to be determined.
Things get more difficult in the presence of predicate subtyping: – the subtype of containing exactly the elements for which the predicate holds. Correspondingly, checking entails proving the proposition , for which a strong prover is (if not required) strongly desirable, and the typing system is immediately undecidable. Additionally, the set of all types for a given term is now a (for all practical purposes) infinite lattice induced by all propositions that hold for and the implications between them.
However, for knowledge management purposes where fully checking the accuracy of content is not strictly necessary, even weak support for computationally difficult features is sufficient for most purposes, especially plain representation. Consequently, in this section we will discuss several subtyping mechanisms that, while not strongly supported by Mmt, are still desirable as purely syntactical features with weak inference support to cover as many situations as possible.
7.2Declared Subtypes and Rule Generators
At its most primitive, a user might want to axiomatically
declare two types to be subtypes of each other. Naively, one might want to implement this by introducing a new constructor such that is inhabitable whenever and are, and adding a simple subtyping rule:
The disadvantage of this naive approach is the existence of a subtyping rule that a) needs to be applicable for arbitrary types and hence be potentially called every time a subtyping judgments is checked, and b) defers to the prover to find an element , which is computationally expensive and fails in the majority of cases anyway (e.g. when are actually equal). Correspondingly, even though adequate, the mere presence of this rule will noticably slow down type checking in general.
To avoid this problem, we can instead implement a change listener, that generates a new subtyping rule for every constant of type which is only applicable on the specific judgment and always returns true if applicable. Additionally, this introduces the constraint on the user that they can only declare two types as subtypes by introducing a constant of the respective -type, which prohibits subtype judgments as arguments in dependent types. This allows the typing system (barring other factors) to stay decidable. The resulting inference rules are simple and listed in Figure 7.1.
A change listener extends the class ChangeListener and needs to implement the following methods:
•
•
•
7.3Intersection Types
In [Pfe93], the authors present an extension of LF by refinement types (sorts) and
intersection types, which introduce a weak subtyping principle while retaining decidability. The following canonical example illustrates the usefulness of these intersection types:
The basic rules for intersection types are given in Figure 7.2.
A rudimentary form of intersection types has been implemented in Mmt. Notably, intersection types as described above still have the drawback that a user has to provide all the intersected types when declaring a new constant, without being able to refine afterwards. For example, the successor function as in Remark 7.3 would require the types and to be declared beforehand, which is counter to the usual order of declarations when implementing natural numbers.
Term declarations as mentioned above could potentially be used to add additional refinement types to a constant after its declaration.
7.4Predicate Subtypes
The type corresponds to the subtype of containing exactly those elements for which the predicate holds. In the presence of Judgments-as-Types, this corresponds to the type of elements for which the dependent type is inhabited – i.e. checking a term against the type entails checking and the existence of a witness .
Given an element , we should be able to obtain a witness , hence we add an additional symbol .
The remaining rules can be easily derived from this intended semantics:
The rudimentary implementation for predicate subtypes in Mmt based on these rules is used e.g. for our formalization of the PVS logic, described in Chapter 10.
Chapter 8
Record Types and Models
In the area of formal systems like type theories, logics, and specification and programming languages, various language features have been studied that allow for inheritance and modularity, e.g., theories, classes, contexts, and records. They all share the motivation of grouping a list of declarations into a new entity such as in . The basic intuition behind it is that behaves like a product type whose values are of the form . Such constructs are indispensable already for elementary applications such as defining the algebraic structure of Semilattices (as in Figure 8.1), which we will use as a running example.
Many systems support stratified grouping (where the language is divided into a lower level for the base language and a higher level that introduces the grouping constructs) or integrated grouping (where the grouping construct is one out of many type-forming operations without distinguished ontological status), or both. The names of the grouping constructs vary between systems, and we will call them theories and records in this chapter. An overview of some representative examples is given in Figure 8.2.
The two approaches have different advantages. Stratified grouping permits a separation of concerns between the core language and the module system. It also captures high-level structure well in a way that is easy to manage and discover in large libraries, closely related to the advantages of the little theories approach [FGT92a]. But integrated grouping allows applying base language operations (such as quantification or tactics) to the grouping constructs. For this reason, the (relatively simple) stratified Coq module system is disregarded in favor of records in major developments such as [Mat].
Allowing both features can lead to a duplication of work where the same hierarchy is formalized once using theories and once using records. A compromise solution is common in object-oriented programming languages, where classes behave very much like stratified grouping but are at the same time normal types of the type system. We call this internalizing the higher level features. While combining advantages of stratified and integrated grouping, internalizing is a very heavyweight type system feature: stratified grouping does not change the type system at all, and integrated grouping can be easily added to or removed from a type system, but internalization adds a very complex type system feature from the get-go. It has not been applied much to logics and similar formal systems: the only example we are aware of is the FoCaLiZe [Har+12] system.A much weaker form of internalization is used in OBJ and related systems based on stratified grouping: here theories may be used as (and only as) the types of parameters of parametric theories. Most similarly to our approach, OCaml’s first-class modules internalize the theory (called module type in OCaml) as the type ; contrary to both OO-languages and our approach, this kind of internalization is in addition and unrelated to integrated grouping.
In any case, because theories usually allow for advanced declarations like imports, definitions, and notations, as well as extra-logical declarations, systematically internalizing theories requires a correspondingly expressive integrated grouping construct. Records with defined fields are comparatively rare; e.g., present in [Luo09] and OO-languages. Similarly, imports between record types and/or record terms are featured only sporadically, e.g., in Nuprl [Con+86], maybe even as an afterthought only.
Finally, note a related trade-off that is orthogonal to our development: even after choosing either a theory or a record to define grouping, many systems still offer a choice whether a declaration becomes a parameter or a field. See [SW11] for a discussion.
|
|
||
|
|
Name of feature
|
|
|
System
|
stratified
|
integrated
|
|
|
||
|
ML
|
signature/module
|
record
|
|
C++
|
class
|
class, struct
|
|
Java
|
class
|
class
|
|
Idris [Bra13]
|
module
|
record
|
|
|
||
|
Coq [Coq15]
|
module
|
record
|
|
HOL Light [Har96]
|
ML signatures
|
records
|
|
Isabelle [Wen09]
|
theory, locale
|
record
|
|
Mizar [Miz]
|
article
|
structure
|
|
PVS [ORS92]
|
theory
|
record
|
|
OBJ [Gog+93]
|
theory
|
|
|
FoCaLiZe [Har+12]
|
species
|
record
|
|
|
Figure 8.2: Stratified and Integrated Groupings in Various Systems
This chapter presents the first formal system that systematically internalizes theories into record types. The central idea is to use an operator that turns the theory into the type , which behaves like a record type. We take special care not to naively compute this record type, which would not scale well to the common situations where theories with hundreds of declarations or more are used. Instead, we introduce record types that allow for defined fields and merging so that preserves the structure of .
This approach combines the advantages of stratified and integrated grouping in a lightweight language feature that is orthogonal to and can be easily combined with other foundational language features. Concretely, it is realized as a module in the Mmt framework. By combining our new modules with existing ones, we obtain many formal systems with internalized theories. In particular, our typing rules conform to the abstractions of Mmt so that Mmt’s type reconstruction [Rab17a] is immediately applicable to our features.
8.1Groupings in Formal Languages
Languages can differ substantially in the syntax and semantics of these constructs. Our interest here is in one difference in particular, which we call the difference between stratified and integrated grouping.
8.1.1Analysis
With stratified grouping, the language is divided into a lower level for the base language and a higher level that introduces the grouping constructs. For example, the SML module system is stratified: it uses a simply typed -calculus at the lower level and signatures for the type-like and structures for the value-like grouping constructs at the higher level. Critically, the higher level constructs are not valid objects at the lower level: even though signatures behave similarly to types, they are not types of the base language. With integrated grouping, only one level exists: the grouping construct is one out of many type-forming operations of the base language with no distinguished ontological status. For example, SML also provides record types as a grouping construct that is integrated with the type system.
Stratified languages have the advantage that they can be designed in a way that yields a conservativity property: all higher level features can be seen as abbreviations that can be compiled into the base language. This corresponds to a typical historical progression where a simple base language is designed first and studied theoretically (e.g., the simply-typed -calculus) and grouping is added later when practical applications demand it. But they have the disadvantage that they tend towards a duplication of features: many operations of the lower level are also desirable at the higher level. For example, SML functors are essentially functions whose domain and codomain are signatures, a duplication of the function types that already exist in the base language. In logics, this problem is even more severe because quantification and equality (and eventually tactics, decision procedures etc.) quickly become desirable at the higher level as well, at which point a duplication of features tends to become infeasible. A well-known example of this trap is the stratified Coq module system (inspired by SML), which practitioners often dismiss in favor of using record types, most importantly in the mathematical components project [Mat].
This may lead us to believe that record types are the way to go — but this is not ideal either. Record types usually do not support advanced declarations like imports, definitions, and notations, which are commonplace in stratified languages and indispensable in practice. Depending on the system, record types may also forbid some declarations such as type declarations (which would require a higher universe to hold the record type), dependencies between declarations (which would require dependent types), and axioms (which do not fit the record paradigm in systems that do not use a propositions-as-types design). And complex definition principles such as for inductive types and recursive functions are often placed into a stratified higher level just to handle their inherent difficulty. Moreover, stratified grouping has proved very appropriate for organizing extra-logical declarations such as prover instructions (e.g., tactics, rewrite rules, unification hints) examples, sectioning, comments, and metadata. While some systems use files as a simple, implicit higher level grouping construct, most systems use an explicit one. The exalted status of higher level grouping also often supports documentation and readability because it makes the large-scale structure of a development explicit and obvious. This is particularly helpful when formalizing software specifications or mathematical theories, whose structure naturally corresponds to those offered by higher-level grouping. In our work on integrating theorem prover libraries (see Part III), my colleagues at KWARC and me have experienced that this correspondence makes it much easier to compare and integrate different stratified formalizations of the same concepts.
For an in-depth discussion of stratified and integrated groupings in various languages, see [MRK].
8.2Record Types with Defined Fields
We now introduce record types as an additional module of our framework. The basic intuition is that and construct record types and terms. We call a context fully typed resp. defined if all fields have a type resp. a definition. In , must be fully typed and may additionally contain defined fields. In , must be fully defined; the types are optional and usually omitted in practice.
Because we frequently need fully defined contexts, we introduce a notational convention for them: a context denoted by a lower case letters like is always fully defined. In contrast, a context denoted by an upper case letter like may have any number of types or definitions.
We extend our grammar as in Figure 8.3.
Before stating the rules, we introduce a few critical auxiliary definition:
Our rules for records are given in Figure 8.4. We remark on a few subtleties below.
•
•
•
•
•
•
•
Note that it does not matter how the fields of the record are split into and as long as contains all fields that the declaration of depends on.
Proof.Let be a fixed well-typed context. We need to show that for any normal expression the inferred type is the most specific one, meaning if , then for any with we have .
If the only type checking rule applicable to a term is an inference rule, then the only way for to check against a type which is not the inferred type is by first inferring and then checking , so in these cases the claim follows by default.
By induction on the grammar:
and , then , which is principal by default.
then , which is principal by default.
is untyped.
then , where , both of which are principal by default.
then for some we have , which is principal by default.
then , where are both principal types and for well-typedness needs to hold. Since is normal, does not simplify to a lambda-expression and is principal by default.
then , where , both of which are unique and hence principal.
then , wheren contains the exact same variables, but with all types inferred (and by induction hypothesis principal). For to check against a type, it has to have the form , hence we need to show that if , then .
Consider the type checking rule for records in Figure 8.4 and let . Since , we have (and if is defined in also ) and since is inferred from we have in , where by hypothesis is the principal type of and hence .
As a result, , therefore and and hence , which makes the principal type of .
Since is normal, we have for some . Since the latter is by hypothesis the principal type of , for to typecheck against some it needs to be the case that type checks against some and holds by the principal type of .
In analogy to function types, we can derive the subtyping properties of record types. We introduce context subsumption and then combine horizontal and vertical subtyping in a single statement.
Intuitively, means that everything of is also in . That yields:
Proof.Assume . We need to show . By the type checking rule in Figure 8.4, for any , we need to show that (and if applicable ).
By definition of , since , we have and , and if is defined in the required equality holds as well, so the type checking rule proves and the claim follows.
Merging RecordsWe introduce an advanced operation on records, which proves critical for both convenience and performance: Theories can easily become very large containing hundreds or even thousands of declarations. If we want to treat theories as record types, we need to be able to build big records from smaller ones without exploding them into long lists. Therefore, we introduce an explicit merge operator on both record types and terms.
In the grammar, this is a single production for terms:
The intended meaning of is given by the following definition:
Note that is an asymmetric operator: While must be well-typed (relative to some ambient context), may refer to the names of and is therefore not necessarily well-typed on its own.
We do not define the semantics of via inference and checking rules. Instead, we give equality rules that directly expand into when possible:
In practice, we want to avoid using the computation rules for whenever possible. Therefore, we prove admissible rules (i.e., rules that can be added without changing the set of derivable judgments) that we use preferentially:
It is possible and important in practice to also define when the types/definitions in and are provably equal. We omit that here for simplicity.
Proof.
•
If and are well-typed record types, then . By definition of , any hence has all fields defined that are required by both and and the other way around. •
By the rules for , for and we get and if and , then (since ) we have and . As can easily be verified, it follows that , and hence .
Inspecting the type checking rule in Figure 8.4, we see that a record of type must repeat all defined fields of . This makes sense conceptually but would be a major inconvenience in practice. The merging operator solves this problem elegantly as we see in the following example:
8.3Internalizing Theories
For the purposes of this section, let be the global context of available modules.
We can now add the internalization operator, for which everything so far was preparation. We add one production to the grammar:
The intended meaning of is that it turns a theory into a record type and a morphism into a function . For simplicity, we only state the rules for the case where all include declarations are at the beginning of theory/morphism:
where we use the following abbreviations:
•
In the rule for theories, is the biggest universe occurring in any declaration transitively included into , i.e., (undefined if any argument is). •
In the rule for morphisms, is the result of substituting in every reference to a declaration of in with . In the rule for morphisms, the occurrence of may appear redundant; but it is critical to (i) make sure all defined declarations of are part of the record and (ii) provide the expected types for checking the declarations in .
The basic properties of are collected in the following theorem:
Proof.
•
Follows immediately by the computation rule for . •
Follows immediately by the computation rule for and the type checking rule for . •
Follows immediately by the computation rule for and Theorem 8.3. An immediate advantage of is that we can now use the expression level to define expression-like theory level operations. As an example, we consider the intersection of two theories, i.e., the theory that includes all theories included by both and . Instead of defining it at the theory level, which would begin a slippery slope of adding more and more theory level operations, we can simply build it at the expression level:
where the are all theories included into both and .
Note that the computation rules for are efficient in the sense that the structure of the theory level is preserved. In particular, we do not flatten theories and morphisms into flat contexts, which would be a huge blow-up for big theories.
However, efficiently creating the internalization is not enough. is defined via , which is itself only an abbreviation whose expansion amounts to flattening. Therefore, we establish admissible rules that allow working with internalizations efficiently, i.e., without computing the expansion of :
Note that because depends on the syntactic structure of and , it only approximates the least upper bound of and and is not stable under, e.g., flattening of and . But it can still be very useful in certain situations.
The computation of may look like it requires flattening. But it is easy to compute and cache its value for every named theory.
The first rule in Theorem 8.5 uses the modular structure of to check at type . If is of the form , this is no faster than flattening all the way. But in the typical case where is also formed modularly using a similar structure as , this can be much faster. The second rule performs the corresponding type inference for an element of that is formed following the modular structure of . In both cases, the last premise is again only needed to make sure that does not contain ill-typed fields not required by . Also note that if we think of as a colimit and of elements of as morphisms out of , then the second rule corresponds to the construction of the universal morphisms out of the colimit.
In practice, these substitutions are easy to implement without flattening because we can cache for every theory which theories it includes and which names it declares.
Example 8.4 is still somewhat artificial because the involved theories are so small. But the effect pays off enormously on larger theories.
Additionally, we can explicitly allow views within theories into the current theory. Specifically, given a theory , we allow a view
the codomain of which is the containing theory (up to the point where is declared). This view induces a view in the top-level context , but importantly, within (and its corresponding inner context ) every variable in is defined via a valid term in . Correspondingly, is – in context – a constant function which we can consider as an element of directly.
This allows for conveniently building instances of and all checking for well-formedness is reduced to structurally checking the view to be well-formed, effectively carrying over all efficiency advantages of structure checking and modular development of theories/views:
Proof.We consider an abbreviation for . Since all definitions in are well-typed terms in context , the record does not actually occur anywhere in the simplified application , which makes this expression well-typed.
8.4Implementation
The implementation of record types and the can be found at [LFX]. They are used extensively in the Math-in-the-Middle archive (see Section 3.4).
For a particularly interesting example that occurs in MitM, consider the theories for modules and vector spaces (over some ring/field) given in Listing 8.1 to Listing 8.4, which elegantly follow informal mathematical practice. Going beyond the syntax introduced so far, these use parametric theories. Our implementation extends to parametric theories as well, namely in such a way that e.g. and correspondingly for fields. Thus, we obtain
and, e.g., , where vectorspace, module, field and ring are all -types.
Because of type-level parameters, this requires some kind of parametric polymorphism in the type system. For our approach, the shallow polymorphism module that is available in PLF (see Remark 4.6) is sufficient.
Formation:
Introduction:
Elimination:
Type checking:
Equality checking (extensionality):
Computation:
Figure 8.4: Rules for Records
Chapter 9
Conclusion and Additional Features
The features presented in this part, collectively, yield a logical framework capable of representing the logical foundations of most formal systems encountered in practice. Our modular approach allows for picking and choosing the required features for a given formalization in a compositional manner, while avoiding the potential overhead of unnecessary rules for a given formalization.
Additional FeaturesNotably, many formal systems offer additional features as “syntactic sugar”, with an abbreviation-like semantics that can already be fully represented in the underlying logic, but which allow for formalizing content more conveniently. Examples include record and function updates in PVS (e.g. “ is defined as the record , except for field , which has value instead”), let-operators that introduce new variables as abbreviations for complex expressions, or sections in Coq (where local variables are introduced as constants, references to which are lambda-abstracted away when closing a section).
In the interest of preserving the syntactic representation of an imported library as much as possible, we prefer adding these features in the formalization of a system’s foundation. Due to their trivial semantics, these features rarely pose a challenge for implementation, and because they can be elaborated away (and usually are in the system itself during checking), they do not introduce hurdles for library integration.
We have implemented some of these convenience features, including a let-operator, an object-level substitution function, a primitive polymorphic type of lists, and Coq-like sections, the latter of which is very naturally implemented as a structural feature and used in our import of the Coq library [MRS]. Furthermore, Fulya Horozal previously implemented an extension of LF with finite sequences and flexary operators [Hor14].
Module-Level ExtensionsThe -operator described in Chapter 8 additionally uses Module-level expressions (namely references to theories), but is still a rule-based object-level typing feature of the underlying logic. However, it is also possible to extend Mmt’s module system itself in various ways. These are (regarding their implementation) rather recent additions to the Mmt system and are not central to this thesis, however, they offer interesting extensions for the goal of this part. In particular, module-level features are entirely orthogonal to the logic-level typing feature discussed in this part; hence they are intrinsically compatible with the modular development approach central to this thesis, and composable with all features herein:
•
•
•
In addition to allowing the formalization of the foundations of formal systems, our modular logical framework is used as a basis for the Math-in-the-Middle library (see Section 3.4), which serves as a case study and explorative playground for evaluation and inspiration for additional features.
Additionally, the latter allows us to experiment with combining and unifying various different approaches and combinations of features, e.g. -types for theories defined via theory combinators that are the codomains of implicit morphisms, or identifying natural numbers as a -type with a declarative implementation using the Peano axioms, and a separate type populated by literals.
Part III
Translating Mathematical Libraries into a Universal Format
To integrate formal libraries from various sources and to implement generic knowledge management services, as is one of the objectives of this thesis (see Section 3.5), it is necessary to have a unifying framework and language in which these libraries are represented. Naturally, OMDoc/Mmt is (due to its generality and modularity) the prime candidate for such a framework. This Part covers the process of translating one library from an external system into the OMDoc/Mmt language.
The OAF project (see Section 3.2) in particular focuses on integrating libraries from theorem prover systems; however, the methodology involved generalizes easily to the purposes of the OpenDreamKit project (see Section 3.3), where the aim is to integrate databases of mathematical objects and their properties (e.g. finite groups), computer algebra systems and related systems. Together, they cover three aspects of the tetrapod (see Chapter 1), namely inference, tabulation and computation. Additionally, the Mmt system itself manages the organization aspect.
In all settings, the process involved in translating a library from system to OMDoc/Mmt entails the following steps:
1.
2.
3.
There is a continuum of possible translations, ranging from perfect adequacy to mere representation. In the best case, we can fully type check the result of the translation and the precise semantics of the original content is preserved under translation. In the worst case, we obtain a representation of the symbols in the original library as untyped and undefined constants. Ideally we want the former, however, depending on the specifics of the system, this might be impossible to achieve without reimplementing the entire system within Mmt. For example, a system with predicate subtypes and a powerful automated prover will usually rely on the latter to type check contents in a manner that can only be reproduced with a similarly powerful prover. In the case of (untyped) computer algebra systems, it might be impossible to check whether a given expression in the language of the system is even well-formed without passing it back to the system itself and evaluating the result.
However, it should be noted that for many knowledge management services such as alignments (see Chapter 14) or (in a limited form) content translation (see Chapter 15), even mere representation is sufficient to obtain useful results. From that point of view, an adequate translation is not strictly necessary, but usually the usefulness of generic services strongly correlates with the amount of details and structure preserved in the translated library.
In this thesis we only consider the statements in a given formal library (declarations, definitions, theorems, axioms) – i.e. we do not cover proofs or specific implementations of methods in computer algebra system. Importing proofs poses additional challenges and requires an adequate proof language sufficiently generic to subsume the various ways proofs can be represented in formal systems, if they can be exported from the system at all. To the best of my knowledge, such a generic proof language that can serve as an adequate target for translations from theorem prover systems does not yet exist. All knowledge management services presented in this thesis consequently do not benefit from any knowledge about proofs, other than (potentially) the binary information whether a statement is proven at all and (possiby) dependency management.
The methodology described in this part has been applied to various systems and libraries by several people, resulting in OMDoc/Mmt imports for Mizar [Ian+13], HOL Light [KR14], TPTP [Sut09], IMPS [Bet18], Isabelle (as-of-yet unpublished), Coq [MRS] and PVS [Koh+17c]. As a representative example, the latter is covered in detail in Chapter 10. Moving on to less formal corpora, Chapter 11 demonstrates how to handle databases of mathematical objects, exemplary the LMFDB, and Chapter 12 covers computer algebra systems, using the GAP and Sage systems as examples.
Chapter 10
Integrating Theorem Prover Libraries - PVS
10.1Introduction and Preliminaries
PVS [ORS92] is a verification system, combining language expressiveness with automated tools. Its language is based on higher-order logic, and is strongly typed. It includes types and terms for concepts such as: numbers, records, tuples, functions, quantifiers, and recursive definitions. Full predicate subtypes are supported, which makes type checking undecidable; PVS generates type obligations (TCCs) as artefacts of type checking. For example, division is defined such that the second argument is nonzero, where nonzero is defined:
Note that functions in PVS are total; partiality is only supported via subtyping.
Beyond this, the PVS language has structural subtypes (i.e., a record that adds new fields to a given record), dependent types for records, tuples, and functions, recursive and co-recursive datatypes, inductive and co-inductive definitions, theory interpretations, and theories as parameters, conversions, and judgements that provide control over the generation of proof obligations. Specifications are given as collections of parameterized theories, which consist of declarations and formulas, and are organized by means of imports.
The PVS prover is interactive, but with a large amount of automation built in. It is closely integrated with the type checker, and features a combination of decision procedures, including BDDs, automatic simplification, rewriting, and induction. There are also rules for ground evaluation, random test case generation, model checking, and predicate abstraction. The prover may be extended with user-defined proof strategies.
PVS has been used as a platform for integration. It has a rich API, making it relatively easy to add new proof rules and integrate with other systems. Examples of this include the model checker, Duration Calculus, MONA, Maple, Ag, and Yices. The system is normally used through a customized Emacs interface, though it is possible to run it standalone (PVSio does this), and PVS features an XML-RPC server (developed independently of the work presented here) that will allow for more flexible interactions. PVS is open source, and is available at .
As an example, Figure 10.1 gives a part of the PVS theory defining equivalence closures on a type in its original syntax. PVS uses upper case for keywords and logical primitives; square brackets are used for types and round brackets for term arguments. The most important declarations in theories are
•
•
•
10.2Formalizing Foundations
To define the language of PVS in Mmt, we carry out two steps.
Firstly, we choose a suitable logical framework by picking the necessary features presented in Part II. Notably, we include three features: anonymous record types (see Chapter 8), predicate subtypes (see Chapter 7), and imports of multiple instances of the same parametric theory. The latter is achieved by a structural feature (see Section 6.3) that elaborates into the lambda-abstracted declarations of the imported theory.
Then we use this logical framework to define the Mmt theory for PVS. Listing 10.1 shows the most fundamental constants of this theory.
We begin with a definition of PVS’s higher-order logic using only LF features. This includes dependent product and function types, classical booleans, and the usual formula constructors (see Listing 10.1). This is novel in how exactly it mirrors the syntax of PVS (e.g., PVS allows multiple aliases for primitive constants) but requires no special Mmt features.
We declare three constants for the three types of built-in literals together with Mmt rules for parsing and typing them. Using the new framework features, we give a shallow encoding of predicate subtyping (see Listing 10.2 for the new typing rule), a shallow definition of anonymous record types, as well as new declarations for PVS-style inductive and co-inductive types.
Contrary to typical dependently-typed languages, PVS does not allow declaring dependent base types, but predicate subtyping can be used to introduce types that depend on terms. Interestingly, this is neither weaker nor stronger than the dependent types in typical calculi.
10.3Importing Libraries
The PVS library export required three separate developments:
Firstly, Sam Owre has extended PVS with an XML export. This is similar to the L
A
T
E
X extension in PVS, which is built on the Common Lisp Pretty Printing facility. The XML export was developed in parallel with a Relax NG specification for the PVS XML files. Because PVS allows overloading of names, infers theory parameters, and automatically adds conversions, the XML generation is driven from the internal type-checked abstract syntax, rather than the parse tree. Thus the generated XML contains the fully type-checked form of a PVS specification with all overloading disambiguated. Future work on this will include the generation of XML forms for the proof trees. Figure 10.2 exemplary shows the (slightly simplified) XML representation of the PVS theory presented in Figure 10.1.
Secondly, Florian Rabe documented the XML schema used by PVS as a set of case classes in Scala and wrote a generic XML parser in Scala that generates a schema-specific parser from such a set of inductive types (see Figure 10.3 for part of the specification). That way any change to the inductive types automatically changes the parser. While seemingly a minor implementation detail, this was critical for feasibility because the XML schema changed frequently along the way.
Thirdly, I wrote an Mmt plugin that parses the XML files generated by PVS and systematically translates their content into OMDoc/Mmt, using the symbols from my formalization of the PVS logic. This includes creating various generic indexes that can be used later for searching the content.
All processing steps preserve source references, i.e., URLs that point to a location (file and line/column) in a source file (the quatruples of numbers at place= in Figure 10.2 and <link rel="...?sourceRef" in Figure 10.4).
The table in Figure 10.5 gives an overview of the sizes of the involved libraries and the run times of the conversion steps. We note that the XML encoding considerably increases the size of representations. This is due to two effects: the internal, disambiguated form contains significantly more information than the user syntax (e.g. theory parameter instances and reconstructed types), and XML as a machine-oriented format is naturally more verbose. Furthermore, OMDoc uses OpenMath for term structures, which again increases file size. While in practice the file sizes are no problem for the Mmt tools presented here, the analogous import for the Isabelle libraries due to Makarius Wenzel has prompted us to compress the OMDoc files by default, significantly reducing their sizes. The Mmt system can read the compressed files directly without need for a user to extract them manually.
Figure 10.3: The Scala-Specification of PVS Constant Declarations for XML Parsing
|
|
||||||
|
|
PVS source
|
PVS XML
|
XML OMDoc
|
|||
|
|
size/gz
|
check time
|
result size/gz
|
run time
|
result size/gz
|
run time
|
|
|
||||||
|
Prelude
|
189.7/46.6kB
|
33s
|
23.5/.67MB
|
11s
|
83.3/1.6MB
|
3m41s
|
|
|
||||||
|
NASA Lib
|
1.9/.426MB
|
23m25s
|
387.2/8.9MB
|
3m11s
|
2.5/.04GB
|
58m56s
|
|
|
Figure 10.5: File Sizes of the PVS Import at Various Stages
Chapter 11
Integrating External Databases (LMFDB)
Having covered importing fully formal theorem prover libraries, we will now turn our attention to systems, where the semantics of the imported ontology is less precise. Specifically, we will look at our methodologies to integrate external databases of mathematical objects (exemplarily the LMFDB) and computer algebra systems (examplarily the GAP and Sage systems). In other words, the tabulation and computation aspects of the tetrapod (see Chapter 1).
Integrating these into the Mmt system was done as part of the OpenDreamKit project (see Section 3.3) with the aim to facilitate data exchange and remote procedure calls between the systems, using the Math-in-the-Middle approach (MitM, see Section 3.4).
11.1LMFDB Knowledge and Interoperability
11.1.1Introduction
The -functions and modular forms database is a project involving dozens of mathematicians who assemble computational data about -functions, modular forms, and related number theoretic objects. The main output of the project is a website, hosted at , that presents this data so that it can serve as a reference for research efforts, and is accessible for postgraduate students. The mathematical concepts underlying the LMFDB are complex and varied, and a large amount of effort has been focused on how to relay knowledge, such as mathematical definitions and their relationships, to data and software. For this purpose, the LMFDB has developed so-called knowls, which are a technical solution to present L
A
T
E
X-encoded information interactively, heavily exploiting the concept of transclusion. The end result is a very modular and highly interlinked set of definitions in mathematical vernacular which can be easily anchored in vastly different contexts, such as an interface to a database, to browsable data, or as constituents of an encyclopedia [Lmfa]. The LMFDB code is primarily written in Python, with some reliance on Sage for the business logic. The backend uses the database system PostgreSQL. Again, due to the complexity of the objects considered, many idiosyncratic encodings are used for the data. This makes the whole data management lifecycle particularly tricky, and dependent on different select groups of individuals for each component.
As the LMFDB spans the whole “vertical” workflow, from writing software, to producing new data, up to presenting this new knowledge, it is a perfect test case for a large scale case study of the MitM approach. Conversely, a semantic layer would be beneficial to integrating its activities across data, knowledge and software.
11.2Integrating the LMFDB with Math-in-the-Middle
Among the components of the LMFDB, elliptic curves stand out as a well-documented data set, and a source of best practices for other areas. We have generated MitM interface theories for LMFDB elliptic curves by (manually) refactoring and flexiformalizing the L
A
T
E
X source of knowls into T
E
X (see Listing 11.1 for an excerpt), which can be converted into flexiformal OMDoc/MMT automatically. The MMT system can already type-check the definitions, avoiding circularity and ensuring some level of consistency in their scope and make it browsable through MathHub.info. Listing 11.1: T
E
X Flexiformalization of an LMFDB Knowl (original: [Lmfb])The first step consisted of translating these informal definitions into progressively more exhaustive MMT formalizations of mathematical concepts (see Listing 11.2) as part of the MitM library. The two representations are coordinated via the theory and symbol names – we can see the T
E
X representation as a human-oriented documentation of the Mmt equivalent. This gives us the necessary formal content to more precisely specify the semantics of the contents of the LMFDB elliptic curves database. The entries in this database represent elliptic curves and contain fields such as their Cremona-label, that uniquely identifies a curve, its -adic generators, conductor, degree, etc.
The core methodology to connect a database to the MitM infrastructure is described in detail in [WKR17]. It relies on the following strategy:
•
•
•
•
•
This methodology is generic and extends beyond the motivating databases in the LMFDB. [BKR] describes how to add the necessary infrastructure to cover additional databases and generate e.g. query interfaces and other services directly from schema theories.
Listing 11.4 shows how we can use the resulting constants in practice. The included theory is the virtual theory generated by the schema theory in Listing 11.3. The constant is computed as described above from the entry in the database with label when it is first referenced. Applying the function to this constant yields an with the value obtained from querying the database.
As a result, we obtain access to all the objects in the databases from within the Mmt system. The objects have globally unique Mmt URIs, and all properties and values for a given object that are stored in the database are obtainable using the Mmt syntax. In other words: The database behaves just like any other collection of Mmt theories and can consequently be used for any of the applications described in this thesis; most importantly those described in Part IV and those relevant for the OpenDreamKit project.
Chapter 12
Integrating Generic Ontologies
12.1Distributed Collaboration with GAP/Sage
Another aspect of interoperability in a mathematical virtual research environment – as is the goal of OpenDreamKit – is the possibility of distributed multisystem computations, where e.g. a given system may decide to delegate certain subcomputations or reasoning tasks to other systems.
There are already a variety of peer-to-peer interfaces between systems in the OpenDreamKit project (see Figure 3.3), which are based on the handle paradigm; for example Sage includes, among others, interfaces for GAP, Singular, and PARI. In this paradigm, when a system delegates a calculation to a system , the result of the calculation is not converted to a native object; instead just returns a handle (or reference) to the object . Later, can run further calculations with by passing it as argument to functions or methods implemented by . Some advantages of this approach are that we can avoid the overhead of back and forth conversions between and , and that we can manipulate objects of from , even if they have no native representation in .
The next desirable feature is for the handle to behave in as if it was a native object; in other words, one wants to adapt the API satisfied by in to match the API for the same kind of objects in . For example, the method call on a Sage handle h to a GAP object G should trigger in GAP the corresponding function call .
This can be implemented using the classical adapter pattern, mapping calls to Sage’s method to corresponding GAP methods. Adapter classes have already been implemented for certain types of objects, like Sage’s or . However, this implementation lacks modularity: for example, if h is a handle to a mere set S, Sage cannot use the adapter method that maps to , because this adapter method is only available in the above two adapter classes.
To get around this problem, Nicolas M. Thiéry and others have worked on a more semantic integration, where adapter methods are made aware of the type hierarchies of the respective systems, and defined at the highest available level of generality, as in Listing 12.1.
Listing 12.1: A Semantic Adapter Method in Sage
This peer-to-peer approach however does not scale up to a dozen systems. This is where the Math-in-the-Middle paradigm comes to the rescue. With it, the task is reduced to building interface theories and interface views into the core MitM ontology in such a way that the adapter pattern can be made generic in terms of the MitM ontology structure, without relying on the concrete structure of the respective type systems. Then the adapter methods for each peer-to-peer interface can be automatically generated. In our example the adapter method for can be constructed automatically as soon as the MitM interface views link the function in the Sage interface theory on Sets with the function in the corresponding interface theory for GAP.
Exporting the GAP Knowledge: Type System DocumentationThe GAP type system encodes a wealth of mathematical knowledge, which can influence method selection. For example establishing that a group is nilpotent will allow for more efficient methods to be run for finding its centre. The main difference between Sage and GAP lies in the method selection process. In Sage the operations implemented for an object and the axioms they satisfy are specified by its class which, together with its super classes, groups syntactically all the methods applicable in this context. In GAP, this information is instead specified by the truth-values of a collection of independent filters, while the context of applicability is specified independently for each method (the details are discussed later). Breuer and Linton describe the GAP type system in [BL] and the GAP documentation [Gap] also contains extensive information on the types themselves.
GAP allows some introspection of this knowledge after the system is loaded: the values of those attributes and properties that are unknown on creation, can be computed on demand, and stored for later reuse.
As a first step in generating interface theories for the MitM ontology, GAP developers have implemented tools to access mathematical knowledge encoded in GAP, such as introspection inside a running GAP session, export to JSON to import to MMT, and export as a graph for visualization and exploration. The JSON output of the GAP object system with default packages is currently around 11 Megabytes, and represents a knowledge graph with 540 vertices, 759 edges and 8 connected components, (see Figures 12.1,12.2). If all packages are loaded, this graph expands to 1616 vertices, 2178 edges and 17 connected components.
There is, however, another source of knowledge in the GAP universe: the documentation, which is provided in the GAPDoc format [LN12]. Besides the main manuals, GAPDoc is adopted by 97 out of the 130 packages currently redistributed with GAP. Conventionally GAPDoc is used to build text, PDF and HTML versions of the manual from a common source given in XML. The reference manual has almost 1400 pages and the packages add hundreds more.
The GAPDoc sources classify documentation by the type of the documented object (function, operation, attribute, property, etc.) and index them by system name. In this sense they are synchronized with the type system (which e.g. has the types of the functions) and can be combined into flexiformal OMDoc/MMT interface theories, just like the ones for LMFDB in Section 11.1. This conversion is currently under development and will lead to a significant increase of the scope of the MitM ontology.
As a side-effect of this work, Markus Pfeiffer discovered quite a few inconsistencies in the GAP documentation, which came from a semi-automated conversion of GAP manuals from the T
E
X-based manuals used in GAP 4.4.12 and earlier. In response, he implemented a consistency checker for the GAP documentation, which extracts type annotations from the documented GAP objects and compares them with their actual types. It immediately reported almost 400 inconsistencies out of 3674 manual entries, 75% of which have been eliminated in a subsequent cleanup. 
Figure 12.1: The GAP Knowledge Graph.
Semantics in the Sage Category SystemThe Sage library includes 40k functions and allows for manipulating thousands of different kinds of objects. In any large system it is critical to tame code bloat by
i)
identifying the core concepts describing common behavior among the objects; ii)
implementing generic operations that apply on all objects having a given behavior, with appropriate specializations when performance calls for it; iii)
designing or choosing a process for selecting the best implementation available when calling an operation on some objects. Following mathematical tradition and the precedent of the Axiom, Fricas, or MuPAD systems, Sage has developed a category-theory-inspired “category system”, and found a way to implement it on top of the underlying Python object system [Dev16; SC]. In short, a category specifies the available operations and the axioms they satisfy. This category system models taxonomic knowledge from mathematics explicitly and uses it to support genericity, control the method selection process, structure the code and documentation, enforce consistency, and provide generic tests.
To generate interface theories from the Sage category system, Nicolas Thiéry et al are experimenting with a system of annotations in the Sage source files. Consider for instance the situtation in Figure 12.3 where we have annotated the category in Sage with lines that state correspondences to other interface theories. From these the Sage-to-MMT exporter can generate the respective interface theories and views.
In ongoing experiments, variants of the annotations are tested for annotating existing categories without touching their source files and providing the signature or the corresponding method names in other systems when this information has not yet been formalized elsewhere.
12.2Representing the GAP Ontology in OMDoc/Mmt
To facilitate the kind of integration demanded by the OpenDreamKit project (such as remote procedure calls), we need appropriate representations of the functionalities offered by the targeted systems. In particular, we need to represent the underlying ontologies of the systems.
In the case of GAP, this ontology is based on the notion of filters, as described above: Every object belongs to several categories and satisfies a list of filters, which can be thought of as predicates (e.g. and , jointly specifying that the object is an abelian group). The way a user interacts with the system is by calling operations (e.g. the order of a group) on an object, which has to satisfy certain filters in order for the operation to be applicable. Notably however, each operation is implemented by possibly multiple methods: specific algorithms for computing an operation. The system uses the known filters of an object to determine which specific method to use for a specific operation. For example,the order of a group might be easier to compute if the group is known to be abelian, hence the system would choose a more appropriate method to compute the order of an abelian group than for a group that is not (known to be) abelian. Notably, the system chooses the method automatically; a user only interacts with the system by calling operations.
This notion of filters effectively yields a soft typing system, which we formalize as in Listing 12.2.
The most primitive notions in the GAP ontology are objects and categories, which we represent as LF types. Naturally, GAP uses literals for booleans, integers and real numbers; consequently we introduce new types for these and populate them with literals as well (lines 5–10).To convert our literals to GAP objects, we introduce conversion functions (lines 12–14). These GAP native literals do not occur in the JSON-export; they are needed for most services implemented in the OpenDreamKit project however. For example, they are needed for translating even simple commands such as into the GAP ontology to allow for remote procedure calls.
We formalize filters as functions and effectively use judgments-as-types for the judgment representing “object has filter ”. The -operator corresponds to a conjunction of filters. allows to build the corresponding filter to a given category, conversely, allows to form the category of all objects satisfying a given filter. An operation is considered a property if it returns a boolean value. In this case we can form the corresponding filter that an object satisfies iff the operation returns true on that object.
Using this formalization, we can systematically translate the contents of the JSON-export of the GAP ontology mentioned above into OMDoc/Mmt declarations.
The export contains a JSON object for each category and operation. For categories, it additionally contains the list of implied filters, for example, the category implies filters such as and . Naturally, a category is translated to a constant of type . For each implied Filter , we generate an additional constant of type .
Unfortunately, the current JSON export does not yet contain any information regarding the required filters of an operation, or the filters of the return object. In the course of the work on the export described above, attempts are being made to make those accessible as well. For now, all operations are correspondingly simply typed as , depending on the arity.
While more detailled information regarding the filters would be desirable for documentation purposes, the above import methodology is sufficient to translate GAP objects, operations, and applications of operations to objects into well-formed OMDoc/Mmt expressions.
12.3Representing the Sage Ontology in OMDoc/Mmt
Having covered the GAP ontology already, extending the same methodology to a smiliar system as Sage is in many respects straight forward. Notably however, whereas GAP implements its own fundamental notions for even simple concepts like integers, Sage is a python library, and as such operates on many of python’s datatypes directly. Consequently, we start with a formalization of the python datatypes relevant for our purposes:
Note that since python uses a dynamic type system, we can not assign a fixed type to a given python object. This is reflected by our ontology, which specifies even the constructors for the various types as having type rather than some dependent type on . As with GAP, these datatypes are not needed for the import of the ontology, but rather for services that operate on expressions within the ontology.
For the ontology itself, we use – as with GAP– a generic type .
As mentioned above, knowledge in Sage– and hence in its JSON-export – is organized in categories (e.g. ). A category satisfies certain axioms/properties (which after translating live in the type in Listing 12.4) and implements certain structures (or signatures, which will live in ) – e.g. the category of rational polynomials implements the signature of a ring, and satisfies (among others) the axioms of a commutative ring.
Each category provides certain methods; namely element methods that operate on the elements in an object of the category (e.g. addition or multiplication in a ring), parent methods that operate on an object of the category directly (e.g. its characteristic or degree), and morphism methods that operate on the respective morphisms of the category.
We translate categories directly to OMDoc/Mmt theories. The JSON-export currently provides no further information on neither the axioms nor the structures. Correspondingly, we treat them as atomic objects of the respective type. We collect all axioms and structures occuring during the import and store them in separate generated theories and , which are included in all the theories corresponding to categories. If a category statisfies an axiom or implements a structure , we add to the theory constants of types or , respectively.
As with GAP, we currently have no information about the input or output types (or categories) of methods; hence we are left with translating those to functions , depending on their arity. Again, this yields a sufficient formalization of the functionalities provided by Sage to facilitate the goals of the OpenDreamKit project.
Chapter 13
Conclusion
We have seen how, using the logical frameworks developed in Part II, we can represent libraries (in the broadest sense) of formal systems in OMDoc/Mmt, including both fully formal libraries as obtained by theorem prover systems, as well as the ontologies of less formal systems such as computer algebra systems and databases of mathematical objects.
In Section 13.1 below, we will look at some suggested applications enabled by representing a single (fully formal) library in OMDoc/Mmt; however, in the light of the title of this thesis, we are much more interested in applications enabled across libraries. Consequently, the important result of this part is less the ability to represent a single library, rather than having a universal framework in which multiple libraries/ontologies of various systems can be (and are) represented, as a prerequisite for the knowledge management service described in Part IV. As such, the intended goals of the OpenDreamKit project are much more in line with the aims of this thesis, even though the systems involved therein (covered in Chapters 11 and 12) are less formal than the fully formal – and hence for knowledge management purposes more interesting – libraries discussed in Chapter 10.
13.1Enabled Applications
With the OMDoc/Mmt translation of formal libraries, the originating systems gain access to library management facilities implemented at the OMDoc/Mmt level. There are two ways to exploit this: publishing the converted libraries on a dedicated server, like the MathHub system [MH], or running the OMDoc/Mmt toolstack locally. Both options offer similar functionality, the main difference is the intended audience: the first option is for outside users who want to access the libraries, and the latter is for users who develop new content or refactor the library.
MathHub (see Section 4.1.2) bundles a GitLab-based repository manager with Mmt and various periphery systems into a common, web-based user interface. We commit the exported libraries – exemplarily from PVS– as OMDoc/Mmt files into a repository to make these available via the i) MathHub user interface, ii) Mmt presentation web server, iii) Mmt web services, and iv) the MathWebSearch daemon. All of these components give the user different ways of interacting with the system and content. Below we explore three examples that are directly useful for PVS users, but the services apply similarly to users of other systems.
The local workflow installs OMDoc/Mmt tools on the same machine as PVS. In that case, users are able to browse the current version of the available PVS libraries including all experimental or private theories that are part of the current development. This also enables PVS to use OMDoc/Mmt services as background tools that remain transparent to the PVS user.
In both workflows, OMDoc/Mmt-based periphery systems become available to the PVS user that are either not provided by the PVS tools or in a much restricted way. We will go over the three most important ones in detail.
13.1.1Browsing and Interaction
The transformed PVS content can be browsed interactively in the document-oriented MathHub presentation pages (theories as active documents) and in the Mmt web browser (see Figure 13.1). Both allow interaction with the PVS content via a generic Javascript-based interface. This provides buttons to toggle the visibility of parts computed by PVS – e.g. omitted types and definitions – at the declaration level. The right-click menu shown in Figure 13.1 is specific to the selected sub-formula (highlighted in gray); here we have eight applicable interactions which range from inferring the subformula type via definition lookup to management actions such as registering an alignment to concepts in other libraries. New interactions can be added as they become available in the MMT system.
The Mmt instance in the local workflow provides the additional feature of inter-process communication between PVS and Mmt as a new menu item: the action navigate to this declaration in connected systems. Florian Rabe implemented a listener for this action that forwards the command to PVS via an XML-RPC call at the default PVS port. Correspondingly, Sam Owre implemented an experimental handler in the PVS server that opens the corresponding file in the PVS emacs system and navigates to the relevant line – unfortunately, due to time constraints this functionality has so far not been fully developed and integrated in an official PVS release.
13.1.2Graph Viewer
MathHub includes a theory graph viewer developed by Marcel Rupprecht that allows interactive, web-based exploration of the OMDoc/Mmt theory graphs [RKM17]. It builds on the visjs JavaScript visualization library [VJS], which uses the HTML5 canvas to layout and interact with graphs client-side in the browser.
PVS libraries make heavy use of theories as a structuring mechanism, which makes a graph viewer for PVS particularly attractive. Figure 13.2 shows the full graph in a central-gravity layout induced by the PVS prelude, where we have (manually) clustered the subgraphs for bit vectors and finite sets (the orange barrel-shaped nodes). The lower right corner shows a zoomed-in fragment.
The theory graph allows dragging nodes around to fine-tune the layout. Hovering over a node or edge triggers a preview of the theory. All nodes support the same context menu actions in the graph viewer as the corresponding theories do in the browser above. Thus, it is possible to select a theory in the graph viewer and then navigate to it in the browser or (if run locally) in the PVS system.
13.1.3Search
MathWebSearch [KŞ06] is an OMDoc/Mmt-level formula search engine that uses query variables for subterms and first-order unification as the query language. It is developed independently, but Mmt includes a plugin for generating MathWebSearch index files using its content MathML interface. Thus, any library available to Mmt can be indexed and searched via MathWebSearch. Moreover, Mmt includes a frontend for MathWebSearch so that search queries can be supplied in any format that Mmt can understand, e.g., the XML format produced by PVS.
Mmt exposes the search frontend both in its GUI for humans and as an HTTP service for other systems. Here we use the latter: We have added a feature to the PVS emacs interface that allows users to enter a search query in PVS syntax. PVS parses the query, type-checks it, and converts it to XML. The XML is sent to Mmt, which acts as the mediator between the proof assistant — here PVS — and library management periphery — here MathWebSearch— and returns the search results to PVS.
The PVS user enters the PVS query , where we have extended the PVS syntax with query variables like ?A. After OMDoc/Mmt translation, this becomes the MathWebSearch query in Figure 13.3 — note the additional symbols from LF introduced by the representation in the logical framework. The representation also introduces unknown meta-variables for the domain and range of the function, which become the additional query variables I1 and I1. MathWebSearch returns a JSON record with all results, and we show the first two in Figure 13.4: two occurrences of (instances of) in two declarations in the theory Figure 10.1. The attribute lib_name is the name of the library; by PVS convention, it is empty for the Prelude. The attributes theory_name and name give the declaration that contains the match, and Position gives the path to its subterm that matched the query.
Figure 13.5 shows what the query will look like while doing a PVS proof. The current implementation is just a proof-of-concept — for the mature version the part of PVS that sends the query to the Mmt server and displays the results still has to be implemented thoroughly. But the remaining steps are straightforward.
Future work could potentially exploit this functionality to search specifically for existing theorems that may be helpful in a specific part of an ongoing PVS proof.
13.1.4Querying Across Libraries
Going beyond a single system, we exported relational data for several theorem prover libraries as RDF triples for more advanced queries without relying on the Mmt system (as published in [Con+]). This relational data is already contained in the underlying OMDoc representation of Mmt archives and can thus be easily generated from imported libraries. In conjunction with alignments (which we will discuss in Chapter 14) this allows for conveniently querying for mathematical concepts across different theorem prover libraries using an arbitrary triple store as backend. For example, for the cited paper I set up an instance of Virtuoso Open-Source, providing a SPARQL endpoint. Using the query
Figure 13.3: A Query for Applications of EquivClos
Figure 13.4: A Query Result for Figure 13.3
Figure 13.5: Example for Displaying the Query Result in PVS
Figure 13.6: Virtuoso Output for the Example Query using Alignments
Part IV
Cross-Library Knowledge Management
Now that we have a unifying framework in which many different libraries are represented, we can approach the problem of integrating these libraries with each other, e.g. to translate knowledge between them.
Naturally, these libraries use different foundations; which is reflected in Mmt as the contained theories having different meta theories. Consequently, as a first step one might want to integrate the foundations themselves, i.e. by implementing systematic translations between them.
An obvious challenge arises here, namely that the foundations used by formal systems are usually mutually incompatible. This is obvious for systems using fundamentally different logics, such as set theories vs. type theories, but even if the platonic foundation used by two systems is the same (e.g. higher-order logic), there are subtle differences in the specific implementations – and hence ontologies – of the foundations, that make implementing such translations less straight-forward than one might at first suspect. For example, the systems might offer different additional features (e.g. records, subtyping) where there is no universally valid elimination procedure. Additionally, systems usually offer distinct convenience operations, automations, module systems and conventions, that are suggestive of different approaches and best practices for formalizing content, leading to very different library developments for the same mathematical concept even if the foundation used by the systems is the same.
As a result, even when a translation between foundations is straight-forward (which it usually is not), the result of translating content between libraries on the basis of a translation between the foundations can yield awkward reformalizations of known content completely disconnected from the content already available in the target library.
Consequently, any generic methodology for integrating libraries needs to go beyond – or even entirely bypass – mere foundations and take distinct library developments into account. This part of this thesis presents our approach to library integration on that premise.
First, we introduce the notion of alignments in Chapter 14. This is a binary relation between symbols expressing that the two symbols (possibly from different libraries) denote the same abstract mathematical concept. In the simplest case, we can then translate symbol occurences in expressions across libraries by merely substituting along alignments. We then classify various more complex types of alignments (e.g. “up to argument order” or “up to additional arguments”) that occur in practice and develop a convenient way to specify them.
Chapter 15 generalizes this approach to translating expressions; using alignments wherever possible, but additionally using theory morphisms (within or across libraries) and – as is crucial for translating across different foundations – programmatic translations, which can be supplied for more complex situations.
To avoid having to provide ad-hoc traslation mechanisms between all pairs of libraries, we instead try to use translations between any library and a fixed set of interface theories, in line with the Math-in-the-Middle approach (see Section 3.4). In a library of interface theories, we can implement all possible developments and definitions of the same mathematical concept and connect them via theory morphisms, lifting the more complicated translation problems to a realm governed by a single, flexible foundation using the logical frameworks developed in Part II. Not surprisingly, this methodology is used to implement the functionalities aimed at by the OpenDreamKit project (see Section 3.3) – Section 15.3 shows a real-world use case from the OpenDreamKit community that is covered by our approach.
In Chapter 16, we describe how to automatically find theory morphisms; both within and across different libraries. These can be used to identify overlap between libraries and consequently suggest new alignments and translations between the theories; ideally resulting in a positive feedback loop of ever increasing connections between libraries.
Lastly, Chapter 17 develops a method for using theory morphisms to refactor library content to increase modularity within a given library.
Chapter 14
Alignments
The sciences are increasingly collecting and curating their knowledge systematically in machine-processable corpora. For example, in biology many important corpora take the form of ontologies, e.g., as collected on BioPortal. These corpora typically overlap substantially, and much recent work has focused on integrating them. A central problem here is to find alignments: pairs of identifiers from different corpora that describe the same concept, giving rise to ontology matching [ESC07].
In the certification of programs and proofs, the ontology matching problem is most apparent when trying to use multiple reasoning systems together. For example, Wiedijk [Wie06] explored a single theorem (and its proof) across 17 proof assistants implicitly generating alignments between the concepts present in the theorem’s statement and proof. The Why3 system [Bob+11] maintains a set of translations into different reasoning systems for discharging proof obligations. Each translation must manually code individual alignments of elementary concepts such as integers or lists in order to fully utilize the respective system’s automation potential. But automating the generation and use of alignments, which would be necessary to scale up such efforts, is challenging because the knowledge involves rigorous notations, definitions, and properties, which leads to very diverse corpora with complex alignment options. This makes it very difficult to determine whether an alignment is perfect (we will attempt to define this notion in the next section), or to predict whether an imperfect alignment will work just as well or not at all.
•
•
•
•
•
Translations along alignments will be covered in Chapter 15.
•
One such refactoring technique will be covered in Chapter 17.
Finding AlignmentsEven though we know that numerous alignments exist between libraries, not many alignments are known concretely or have been represented explicitly. Therefore, a major initial investment is necessary to obtain a large library of interface theories and alignments. There are three groups of alignment-finding approaches.
Human-based approaches examine libraries and manually identify alignments. This approach has been pursued ad hoc in various contexts. For example, the library translation of [OS06b] included some alignments for HOL Light and Isabelle/HOL, which were later expanded by Kaliszyk. The Why3 and FoCaLiZe systems include alignments to various theorem provers that they use as backends. Results from this approach will be discussed in Section 14.5.
The remaining two classes use machine learning methods.
Logical approaches align two concepts if they satisfy the same theorems. This cannot directly appeal to logical equivalence because that would require a translation between the corpora. Instead, they compare the theorems that are explicitly stated in the corpora. The theorems should be normalized first to eliminate differences that do not affect logical equivalence. The quality of the results depends on how completely those theorems characterize the respective concepts. In well-curated libraries, this can be very high [MK15]. The Viewfinder presented in Chapter 16 can be interpreted as implementing this approach.
Machine learning–based approaches are inherently based on statistical patterns and hence naturally inexact. The main research in this direction is carried out by Kaliszyk and others [GK14b].
Automatic Search for AlignmentsFinding alignments, preferably automatically, has proved extremely difficult in general. There are three reasons for this: the conceptual differences between logical corpora found in proof assistants, computational corpora containing algorithms from computer algebra systems, narrative corpora that consist of semi-formal descriptions from wiki-related tools; the diversity of the underlying formal languages and tools; and the differences between the organization of the knowledge in the corpora.
While finding alignments automatically is promising for perfect alignments, where two symbols only differ in name but are otherwise used identically, it is a different matter for imperfect alignments. For example, consider binary division which yields undefined or 0 when the divisor is zero, versus a strict division that requires an additional proof-argument that the divisor is nonzero. Here automation becomes much more difficult, because the imperfections often violate the conditions that an automatic approach uses to spot alignments.
I conjecture that the quality of artificial intelligence approaches will be massively improved if they are applied on top of a large set of guaranteed-perfect alignments, besides their obvious use as training data. This is based on two observations:
•
The more alignments we know, the easier it is to find new ones. Consider a typical formalization in system that introduces a new concept relative to some known ones. If perfect alignments to system for the known concepts have already been established, it becomes relatively easy to find the formalization of in , and add an alignment for it. •
It is very difficult to get alignment-finding off-the-ground. Because the foundations of and are often very different, almost nothing looks particularly similar in the absence of any alignments. Deeper alignments will become more apparent only when alignments for fundamental concepts such as booleans, sets and numbers are established. Recently, heuristic methods for automatically finding alignments were developed [GK14b], targeted at integrating logical corpora, which were integrated into our developments in Section 14.1. Independently, Deyan Ginev built a library [GC14] of about 50,000 alignments between narrative corpora including Wikipedia, Wolfram Mathworld, PlanetMath and the SMGloM semantic multilingual glossary for mathematics. For this, the NNexus system indexes the corpora and applies clustering algorithms to discover concepts.
Related WorkAlignments between computational corpora occur in bridges between the run time systems of programming languages. Alignments between logical and computational corpora are used in proof assistants with code generation such as Isabelle [WPN08] and Coq [Coq15]. Here functions defined in the logic are aligned with their implementations in the programming language in order to generate fast executable code from formalizations.
The dominant methods for integrating logical corpora so far have focused on truth-preserving translations between the underlying knowledge representation languages. For example, [KS10] translates from Isabelle/HOL to Isabelle/ZF. [KW10] translates from HOL Light to Coq, [OS06a] to Isabelle/HOL, and [NSM01] to Nuprl. Older versions of Matita [Asp+06a] were able to read Coq compiled theory files. [Cod+11] build a library of translations between different logics.
However, as mentioned in the introduction to this part, most translations are not alignment-aware, i.e., it is not guaranteed that will be translated to even if the alignment is known. This is because and may be subtly incompatible so that a direct translation may even lead to inconsistency or ill-typed results. [OS06a] was — to my knowledge — the first that could be parametrized by a set of alignments. The OpenTheory framework [Hur09] provides a number of higher-order logic concept alignments. In [KR16a], the corpus integration problem is discussed and concluded that alignments are of utmost practical importance. Indeed, corpus integration can succeed with only alignment data even if no logic translation is possible. Conversely, logic translations contribute little to corpus integration without alignment data.
14.1Types of Alignments
Let us assume two corpora with underlying foundational logics . We examine examples for how two concepts from can be aligned. Importantly, we allow for the case where and represent the same abstract mathematical concept without there being a direct, rigorous translation between them.
The types of alignments in this section are purely phenomenological in nature: they exemplify the difficulty of the problem and provide benchmarks for rigorous definitions. While some types are relatively straightforward, others are so difficult that giving a rigorous definitions remains an open problem. This is because alignments ideally legitimize translations from to that replace with . But in many situations these translations, while possible in principle, are much more difficult than simply replacing one symbol with another. The alignment types below are roughly ordered by increasing difficulty of this translation.
Perfect AlignmentIf and are logically equivalent (modulo a translation between and that is fixed in the context), we speak of a perfect alignment. More precisely, all formal properties (type, definition, axioms) of carry over to and vice versa. Typical examples are primitive types and their associated operations. Consider:
then translations between and can simply interchange and .
The above example is deceptively non-trivial for two reasons. Firstly, it hides the problem that and do not necessarily share the symbol . Therefore, we need to assume that there are symbols and , which have been already aligned (perfectly). Such alignments (on the foundations of and ) are crucial for all fundamental constructors that occur in the types and characteristic theorems of the symbols we want to align such as , , , , etc. These alignments can be handled with the same methodology as discussed here. Therefore, here and below, we assume we have such alignments and simply use the same fundamental constructors for and .
Secondly, it ignores that we usually want (and can reasonably expect) only certain formal properties to carry over, namely those in the interface theory in the sense of [KR16a] — i.e. those properties that are still meaningful after abstracting away from the specific foundational logics . We will look at some examples for perfect alignments between symbols that use different but equivalent definitions in Section 14.2.
Alignment up to Argument OrderTwo function symbols can be perfectly aligned except that their arguments must be reordered when translating.
The most common example is function composition, whose arguments may be given in application order () or in diagram order (). Another example is given
Here the expressions and can be translated to each other.
|
|
|
|
Alignment up to Determined ArgumentsThe perfect alignment of two function symbols may be broken because they have different types even though they agree in most of their properties. This often occurs when uses a more fine-granular type system than , which requires additional arguments.
Examples are untyped and typed (polymorphic, homogeneous) equality: The former is binary, while the latter is ternary
The types can be aligned, if we apply to . Similar examples arise between simply- and dependently-typed foundations, where symbols in the latter take additional arguments.
These additional arguments are uniquely determined by the values of the other arguments, and a translation from to can drop them, whereas the reverse translations must infer them – but usually has functionality for that (e.g. the type parameter of polymorphic equality is usually uniquely determined).
The additional arguments can also be proofs, used for example to represent partial functions as total functions, such as a binary and a ternary division operator
Here inferring the third argument is undecidable in general, and it is unique only in the presence of proof irrelevance.
|
|
|
|
Alignment up to Totality of FunctionsThe functions and can be aligned everywhere where both are defined. This happens frequently since it is often convenient to represent partial functions as total ones by assigning values to all arguments. The most common example is division. Two implementations and might both have the type with undefined and .
Here a translation from to can always replace with . The reverse translation can usually replace with but not always. In translation-worthy data-expressions, it is typically sound; in formulas, it can easily be unsound because theorems about might not require the restriction to non-zero denominators.
Alignment for Certain ArgumentsTwo function symbols may be aligned only for certain arguments. This occurs if has a smaller domain than .
The most fundamental case is the function type constructor itself. For example, may be first-order in and higher-order in . Thus, a translation from to can replace with , whereas the reverse translation must be partial.
Another important class of examples is given by subtyping (or the lack thereof). For example, we could have
Alignment up to AssociativityAn associative binary function (either logically associative or notationally right- or left-associative) can be defined as a flexary function, i.e., a function taking an arbitrarily long sequence of arguments. In this case, translations must fold or unfold the argument sequence. For example
All of the above types of alignments allow us to translate expressions between our corpora by modifying the lists of arguments the respective symbols are applied to, even if not always in a straight-forward way. The following types of alignments are more abstract, and any translation along them might be more dependent on the specifics of the symbols under consideration.
Contextual AlignmentsTwo symbols may be aligned only in certain contexts. For example, the complex numbers are represented as pairs of real numbers in some proof assistant libraries and as an inductive data type in others. Then only selected occurrences of pairs of real numbers can be aligned with the complex numbers.
Alignment with a Set of DeclarationsHere a single declaration in is aligned with a set of declarations in . An example is a conjunction in of axioms aligned with a set of single axioms in . More generally, the conjunction of a set of -statements may be equivalent to the conjunction of a set of -statements.
Here translations are much more involved and may require aggregation or projection operators.
Alignment between the Internal and External Perspective on TheoriesWhen reasoning about complex objects in a proof assistant (such as algebraic structures, or types with comparison) it is convenient to express them as theories that combine the actual type with operations on it or even properties of such operations. The different proof assistants often have incompatible mechanisms of expressing such theories including type classes, records and functors, with the additional distinction whether they are first-class objects or not. This roughly corresponds to the distinction between stratified and integrated groupings in Chapter 8.
We define the crucial difference for alignments here only by example. We speak of the internal perspective ( stratified grouping) if we use a theory like
and of the external perspective ( integrated grouping) if we use operations like
Here we have a non-trivial, systematic translation from to . A reverse may also be possible, depending on the details of .
|
|
|
|
Corpus-Foundation AlignmentOrthogonal to all of the above, we have to consider alignments, where a symbol is primitive in one system but defined in another. More concretely, can be built-into whereas is defined in . This is common for corpora based on significantly different foundations, as each foundation is likely to select different primitives. Therefore, it mostly occurs for the most basic concepts. For example, the boolean connectives, integers and strings are defined in some systems but primitive in others, as in some foundations they may not be easy to define.
The corpus-foundation alignments can be reduced to previously considered cases if we follow the approach generally followed in this thesis, where the foundations themselves are represented in an appropriate logical framework. Then is simply an identifier in the corpus of foundations of the framework .
In Mmt, we can bridge these two representations using the -types described in Chapter 8
Opaque AlignmentsThe above alignments focused on logical corpora, partially because logical corpora allow for precise and mechanizable treatment of logical equivalence. Indeed, alignments from a logical into a computational or narrative corpus tend to be opaque: Whether and in what way the aligned symbols correspond to each other is not (or not easily) machine-understandable. For example, if refers to a function in a programming language library, that function’s specification may be implicit or given only informally. Even worse, if is a wiki article, it may be subject to constant revision.
Nonetheless, such alignments are immensely useful in practice and should not be discarded. Therefore, we speak of opaque alignments if refers to a symbol whose semantics is unclear to machines.
Probabilistic AlignmentsOrthogonal to all of the above, the correctness of an alignment may be known only to some degree of certainty. In that case, we speak of probabilistic alignments. These occur in particular when machine-learning techniques are used to find large sets of alignments automatically. This is critical in practice to handle the existing large corpora.
The problem of probabilistically estimating the similarity of concepts in different corpora was studied before in [GK14b]. I briefly restate the relevant aspects in our setting, as described by Thibault Gauthier in [Mül+17b].
Let be the set of top level expressions occurring in , e.g., the types of all constants and the formulas of all theorems. We assume a fixed set of alignments, covering in particular the foundational concepts in and .
Let be the set of all alignments in any . We first calculate an initial vector containing the similarities for each by
Intuitively, an alignment has a high similarity value if it was produced by a large number of rare patterns.
Secondly, we iteratively transform this vector until its values stabilize. The idea behind this dynamical system is that the similarity score of an alignment should depend on the quality of its co-induced alignments. Each iteration step consists of two parts: we multiply the vector with the matrix
which measures the correlation between and , and then (in order to ensure convergence and squash all values into the interval ) apply the function to each component.
14.2Examples of Alignments
An essential requirement for relating logical corpora is standardizing the identifiers so that each identifier in the corpus can be uniquely referenced. It is desirable to use a uniform naming schema so that the syntax and semantics of identifiers can be understood and implemented as generically as possible. Mmt URIs have been specifically designed for that purpose, and Part III shows by example how to systematically generate URIs during importing a library. Additionally, in [Mül+17c] we present URI schemas for a list of selected theorem provers.
Using these URIs with abbreviated proof assistant names, the following presents alignments across proof assistants for two representative concepts. Also included are some alignments to programming languages, which are relevant for code generation. Thousands of other alignments, both perfect and imperfect, can be explored on mathhub [PRA].
Cartesian ProductIn constructive type theory, there are two common ways of expressing the non-dependent Cartesian product. First, if the foundation has inductive types such as the Calculus of Inductive Constructions, it can be an inductive type with one binary constructor. This is the case for:
•
Coq ? Init/Datatypes ? prod.ind •
Matita ? datatypes/constructors ? Prod.ind Second, if the foundation defines a dependent sum type, it is possible to express the Cartesian product as its non-dependent special case:
•
Isabelle ? CTT/CTT ? times In higher-order logic, the only way to introduce types is by using the typedef construction, which constructs a new type that is isomorphic to a certain subtype of an existing type. In particular, most HOL-based systems introduce the Cartesian product by using a unary predicate on :
•
HOLLight ? pair/type ? prod •
HOL4 ? pair/type ? prod •
Isabelle ? HOL/Product ? prod In set theory, it is also possible to restrict dependent sum types to obtain the Cartesian product. This approach is used in Isabelle/ZF:
•
Isabelle ? ZF/ZF ? cart_prod In Mizar the Cartesian product is defined as functor in first-order logic. The definition invloves discharging the well-definedness condition. We defined functor is:
•
Mizar ? ZFMISC_1 ? K2 In PVS, the product type constructor is part of the system foundation:
•
PVS ? foundation.PVS ? tuple_tp Cartesian products appear also in most programming languages and the code generators of various proof assistants do use a number of these:
•
OCaml ? core ? * •
Haskell ? core ? , •
Scala ? core ? , •
CPP ? std ? pair Informal sources that can be aligned are e.g.:
Concatenation of ListsIn constructive type theory (e.g. for Matita, Coq), the append operation on lists can be defined as a fixed point. In higher-order logic, append for polymorphic lists can be defined by primitive recursion, as done by HOL Light and HOL4. Isabelle/HOL slightly differs from these two because it uses lists that were built with the co-datatype package [Bla+14]. PVS and Isabelle/ZF also use primitive recursion for monomorphic lists. In Mizar, lists are represented by finite sequences, which are functions from a finite subset of natural numbers (one-based FINSEQ and zero-based XFINSEQ) with append provided. Concatenation of lists is also common in programming languages.
•
Coq ? Init/Datatypes ? app •
HOLLight ? lists/const ? APPEND •
HOL4 ? list/const ? APPEND •
Isabelle ? HOL/List ? append •
PVS?Prelude.list_props?append •
Isabelle ? ZF/List_ZF ? app •
Mizar ? ORDINAL4 / K1 •
OCaml ? core ? @ •
Haskell ? core ? ++ •
Scala ? core ? ++ 14.3A Standard Syntax for Alignments
Based on the observations of the previous sections, we now define a standard for alignments. Because many of the alignment types described in Section 14.1 are very difficult to handle rigorously and additional alignment types may be discovered in the future, we opt for a very simple and flexible definition.
Concretely, we use the following formal grammar for collections of alignments:
|
Collection
|
::=
|
|
|
Comment
|
::=
|
// String
|
|
NSDef
|
::=
|
namespace String URI
|
|
Alignment
|
::=
|
URI URI
|
Our definition aims at practicality, especially considering the typical case where researchers exchange and manipulate large collections of alignments. Therefore, our grammar allows for comments and for the introduction of short namespace definitions that abbreviate long namespaces. Our grammar represents each individual alignment as a pair of two URIs with arbitrary additional data stored as a list of key-value pairs.
The additional data in alignments makes our standard extensible: any user can standardize individual keys in order to define specific types of alignments. For example, for alignments up to argument order, we can add a key for giving the argument order. Moreover, this can be used to annotate metadata such as provenance or system versions.
Below we standardize some individual keys and use them to implement the most important alignment types from Section 14.1. In all definitions below, we assume that and are the aligned symbols.
Alignments with key subsume the alignment types of perfect alignments (where the direction is ) and the unidirectional types of alignment up to totality of functions or up to associativity, and alignment for certain arguments. The absence of this key indicates those alignment types where no symbol-to-symbol translation is possible, in particular opaque alignments.
Alignments with key subsume the alignment types of alignments up to argument order and of alignment up to determined arguments.
14.4Implementation
I have implemented alignments in the Mmt system. Moreover, I have created a public repository [PRA] and seeded it with a number of alignments (currently ) including the ones mentioned above and below in Section 14.5, the README of this repository furthermore describes the syntax for alignments above as well as the URI schemata for several proof assistants. The Mmt system can be used to parse and serve all these alignments, implement the transitive closure, and (if possible) translate expressions according to alignments (see Chapter 15 for the details). Available alignments are shown in the Mmt browser.
As an example service, I built a prototypical alignment-based math dictionary collecting formal and informal resources. For this we extend the above grammar by the following:
|
Alignment
|
::=
|
String URI
|
This assigns a mathematical concept (identified by the string) to a formal or informal resource (identified by the URI). The dictionary uses the above public repository, so additions to the latter will be added to the former. We have imported the 50,000 conceptual alignments from [GC14], although we chose not to add them to the dictionary yet, since the majority of them are (due to the different intention behind the conceptual mappings in Nnexus) dubious, highly contextual or otherwise undesirable.
Each entry in the dictionary shows snippets from select online resources if available (Figure 14.1), lists the associated formal statements (Figure 14.2) and available alignments between them (Figure 14.3), and allows for conveniently adding new individual URIs to concept entries as well as new formal alignments (Figures 14.1 and 14.4 respectively).
14.5Manually Curated Alignments
As an experiment,we hired two mathematics students at Jacobs University in Bremen – Colin Rothgang and Yufei Liu – to manually comb through libraries of HOL Light, PVS, Mizar and Coq to find alignments. Specifically, they picked the mathematical areas of numbers, sets (as well as lists), abstract algebra, calculus, combinatorics, logic, topology, and graphs as a sample. This produced around 900 declarations overall, from which they constructed interface theories, as presented in Section 15.1. Notably neither of the two students had prior in-depth knowledge about theorem prover systems or their libraries.
Alignments in topology pose some additional difficulties. Firstly, HOL Light defines a topology on some subset of the universal set of a type, whereas PVS defines it on a type directly. Thus, the alignment from HOL Light to the interface theory is unidirectional. Secondly, Mizar does not define the notion of a topology, but instead the notion of a topological space. Therefore, the students aligned all these symbols to two different symbols in an interface theory ( and ) and defined based on .
The set of all alignments they found can be inspected at . Many of these alignments are by now outdated, due to recent developments on Mmt, including an import for Coq (see [MRS]) which had us rethink their Mmt URI schema, and changes in the surface syntax that require the archive of interface theories (discussed in Section 15.1) to be cleaned up and partially reimplemented. However, as an experiment, it shows that finding and implementing alignments manually is surprisingly easy even with very little prior knowledge of the formal systems.
During the course of collecting alignments, Rothgang and Liu have identified the following two aspects to be the most common causes for imperfect alignments:
•
•
Unfortunately, due to recent changes in the Mmt API, the original dictionary is no longer compatible with the current code base and needs to be reimplemented at some point in the future.
|
|
||||
|
Concept
|
PVS (Standard)
|
HOL Light (Standard)
|
Mizar (Standard)
|
Coq (Standard)
|
|
|
||||
|
|
naturalnumbers?naturalnumber
|
nums?nums
|
ORDINAL1?modenot.6
|
Coq.Init.Datatypes?nat
|
|
successor function
|
naturalnumbers?succ
|
nums?SUC
|
ORDINAL1?func.1
|
Coq.Init.Nat?succ
|
|
addition
|
number_fields?+
|
arith?ADD
|
ORDINAL2?func.10
|
Coq.Init.Nat?add
|
|
multiplication
|
number_fields?*
|
arith?MULT
|
ORDINAL2?func.11
|
Coq.Init.Nat?mul
|
|
less than
|
number_fields?
|
arith?
|
XXREAL_0?pred.1
|
Coq.Init.Nat?leb
|
|
|
Table 14.1: Alignments for NaturalNumbers (libraries in brackets)
|
|
||||
|
Concept
|
HOL Light (Standard)
|
Mizar (Standard)
|
||
|
|
||||
|
topology
|
topology_prelim?topology
|
topology?topology
|
PRE_TOPC?modenot.1
|
TopologicalSpaces?TopologicalSpace
|
|
open
|
topology?open?
|
topology?open_in
|
PRE_TOPC?attr.3
|
TopologicalSpaces?open
|
|
closed
|
topology?closed?
|
topology?closed_in
|
PRE_TOPC?attr.4
|
TopologicalSpaces?closed
|
|
interior
|
topology?interior
|
topology?interior
|
TOPS_1?func.1
|
InteriorsClosures?interior
|
|
closure
|
topology?Cl
|
topology?closure
|
PRE_TOPC?func.2
|
InteriorsClosures?closure
|
|
|
Table 14.2: Alignments for Topology (libraries in brackets)
|
|
||||
|
Topic
|
HOL Light
|
PVS
|
Mizar
|
Coq
|
|
|
||||
|
Algebra
|
0/0
|
18/1
|
17/0
|
14/0
|
|
|
||||
|
Calculus
|
15/0
|
14/0
|
16/0
|
5/15
|
|
|
||||
|
Categories
|
0/0
|
0/0
|
9/1
|
5/0
|
|
|
||||
|
Combinatorics
|
24/0
|
15/0
|
1/0
|
1/0
|
|
|
||||
|
Complex Numbers
|
9/2
|
4/6
|
7/2
|
11/2
|
|
|
||||
|
Graphs
|
5/5
|
17/0
|
20/0
|
7/2
|
|
|
||||
|
Integers
|
10/0
|
0/0
|
5/2
|
47/3
|
|
|
||||
|
Lists
|
16/0
|
9/0
|
8/0
|
36/2
|
|
|
||||
|
Logic
|
7/0
|
7/5
|
7/0
|
24/1
|
|
|
||||
|
Natural Numbers
|
19/0
|
8/10
|
9/0
|
34/1
|
|
|
||||
|
Polynomials
|
4/0
|
1/0
|
7/0
|
0/0
|
|
|
||||
|
Rational Numbers
|
0/14
|
2/11
|
0/10
|
14/3
|
|
|
||||
|
Real Numbers
|
13/2
|
3/10
|
7/4
|
12/2
|
|
|
||||
|
Relations
|
4/0
|
16/5
|
18/3
|
1/12
|
|
|
||||
|
Sets
|
23/0
|
28/0
|
18/0
|
19/0
|
|
|
||||
|
Topology
|
15/0
|
10/0
|
9/0
|
17/1
|
|
|
||||
|
Vectors
|
13/0
|
7/0
|
15/0
|
0/0
|
|
|
||||
|
Sum
|
177/23
|
159/48
|
173/22
|
240/42
|
|
|
Table 14.3: Number of Bidirectional/Unidirectional Alignments per Library
Chapter 15
Alignment-based Translations Using Interface Theories
Using alignments, we can equivocate symbols from different libraries with each other. Ideally, in the case of a perfect alignment we can then reduce translation to a one-to-one symbol substitution. However, given a multitude of libraries in our framework, naively approaching the task of aligning them in the first place still means sifting through two libraries in parallel, implying alignment tasks for libraries.
In recent work, our research group has come to understand this problem more clearly and suggested a systematic solution. Firstly, in [KRSC11] and [KR16b], Michael Kohlhase, Florian Rabe and Claudio Sacerdoti Coen developed the idea of interface theories. Using an analogy to software engineering, we can think of interface theories as specifications and of theorem prover libraries as implementations of formal knowledge.
Secondly, in the OpenDreamKit project [Deh+16; ODK] (see Section 3.3) we pursue the same approach (Math-in-the-Middle, see Section 3.4) in the context of computer algebra systems. In this context, we have already developed some interface theories for basic logical operations such as equality, with approximately 300 alignments to theorem prover libraries.
Not surprisingly, the methodology described in this chapter, while in theory originally developed for fully formal libraries originating from theorem prover systems, has consequently been used to realize the objectives of OpenDreamKit as well.
While alignments have the big advantage that they are cheap to find and implement, they have the disadvantage of not being very expressive; in fact, the definition of alignment itself is (somewhat intentionally) vague. In particular when a translation needs to consider foundational aspects beyond the individual system dialects, alignments alone are insufficient. This is where interface theories come into play: given different implementations of the same mathematical concept, their interface theory contains only those symbols that are a) common to all implementations and b) necessary to use the concept (as opposed to formalizing it in detail) – which in practice turn out to be the same thing.
Libraries of interface theories hence must critically differ from typical theorem prover libraries: they must follow the axiomatic method (as opposed to the method of definitional extensions), be written with minimal foundational commitment, and largely not rely on definitions or proofs in order to stay compatible with development approaches based on alternative definitions.
Using interface theories and the Math-in-the-Middle approach, we can see two symbols being aligned via a sequence of consecutive steps of abstraction:
1.
2.
3.
Consider for a simple example the PVS symbol and the HOL Light symbol , we capture this with
•
a symbol for elementhood in a (new) interface theory for sets, •
two alignments of this new symbol with the symbols This yields a star-shaped network as in the diagram in Figure 15.1 with various formal libraries on the outside, which are connected by alignments via representations of their system dialects (lower-case letters) to the interface theory in the center. Note the very deliberate similarity to Figure 3.4 – the primary difference is that we substituted OpenDreamKit systems with OAF systems (see Section 3.5).
15.1Interface Theories
As mentioned in Section 14.5, we had two students (Colin Rothgang and Yufei Liu) collect alignments between various theorem prover libraries. In the course of this project, they also developed interface theories for the symbols they aligned.
As a basis for this experiment, they used the foundational theory for the Math-in-the-Middle archive, a simplified excerpt of which is shown in Listing 15.1, as an interface for basic logical constants.
This theory actually includes most of the features presented in Part II, in order to be as flexible as possible in formalizing content – although most of them were not yet available when the experiment described in this section was originally done.
15.1.1Example: Natural Numbers
Listing 15.2 shows an example of a simple theory of natural numbers, using the theory and the symbols declared therein. Note, that this theory is basically an implementation of the Peano axioms, which can be seen as the interface theory for all possible definitions of a concrete set (or type) of “the” natural numbers.
In Mizar [Miz], which is based on Tarski-Grothendieck set theory, the set of natural numbers is defined as omega, the set of finite ordinals. Arithmetic operations are defined directly on those.
In contrast, in PVS (see Chapter 10) natural numbers are defined as a specific subtype of the integers, which in turn are a subtype of the rationals etc. up to an abstract type which serves as a maximal supertype to all number types. The arithmetic operations are inherited from a subtype of .
These are two fundamentally different approaches to describe and implement an abstract mathematical concept, but for all practical purposes the concept they describe is the same; namely the natural numbers. The interface theory for both variants would thus only contain the symbols that are relevant to the abstract concept itself, independent of their specific implementation – hence, things like the type of naturals, the arithmetic operations and the Peano axioms. The interface theory thus provides everything we need to work with natural numbers, and at the same time everything we know about them independently of the logical foundation or their specific implementation within any given formal system.
However, there is an additional layer of abstraction here, namely that in stating that the natural numbers in Mizar are the finite ordinals we have already ignored the system dialect (in the sense of item 2 in the introduction to this chapter). This step of abstraction (from the concrete definition using only Mizar-specific symbols) yields another interface theory for finite ordinals, which in turn can be aligned not just with Mizar natural numbers, but also e.g. with MetaMath [MeMa], which is built on ZFC set theory.
Figure 15.2 illustrates this situation. Blue arrows point from more detailed theories to their interfaces. The arrows from PVS or Mizar to interfaces merely strip away the system dialects; the arrows within Interfaces abstract away more fundamental differences in definition or implementation.
Consider again Listing 15.2, a possible interface theory for natural numbers. Note, that symbols such as could be defined, but don’t actually need to be. Since they are only interfaces, all we need is for the symbols to exist.
In fact, the more abstract the interface, the less we want to define the symbols – given that there’s usually more than one way to define symbols, definitions are just one more thing we might want to abstract away from completely. There are exceptions to this – note that the symbol is actually defined as the literal . This is because literals themselves are mere Mmt terms, but not symbols with a stable Mmt-URI, which we need for alignments. On the other hand, not having literals excludes those systems where literals are actually used. In this case, providing a definition to the symbols enables aligning both systems with and without literals.
The symbols in this interface theory can then be aligned either with symbols in other formal systems directly, or with additional interfaces in between, such as a theory for Peano arithmetic, or the intersection of all inductive subsets of the real numbers, or finite ordinals or any other possible formalization of the natural numbers.
15.1.2Additional Interface Theories
The foundation independent nature of Mmt allows us to implement interface theories with almost arbitrary levels of detail and for vastly different foundational settings.
We have started a repository of interface theories specifically for translation purposes [Mitb] and also aligned to already existing interfaces (as in the case of arithmetics, see below) in a second and third MathHub repository [Mitc] and [Mita] extending them when necessary.
Crucially, this interface repository contains interface theories for basic type-related symbols like the function type constructors (see Listing 15.3), that are aligned with the respective symbols in HOL Light and PVS. These symbols are so basic as to be primitive in systems based on type theory, and consequently they occur in the vast majority of expressions. To have these symbols aligned is strictly necessary to get any further use of alignments off the ground.
See Section 6.2.1 for more on Literals in Mmt.
This interface theory, like most formalizations of foundations, uses types as terms (via the symbols
Here, a structure is used to include the theory for simple function types in the theory for dependent function types, while providing definitions for the symbols in terms of the latter. This automatically yields a translation from the simple to the dependent variant and demonstrates the advantage of using interface theories for translations: The general problem of converting between (systems using) simple and dependent function types is lifted to the level of the interface theories, where we can use theory morphisms (such as structures) to specify the appropriate translation once and for all; independent of any specific external system.
Table 14.3 shows the total number of alignments the students found for PVS, HOL Light and Mizar. The following are some additional examples of mathematical areas covered by the resulting interface theories. The numbers here reflect the result of the student experiment and refer to the number of symbols actually used for alignments therein; the theories themselves have been partially adapted and significantly extended by now:
Limitscontains 17 symbols related to sequences and limits, including and (metric spaces and their completeness).
Differentiationcontains 4 symbols, namely differentiability in a point and on a set and the derivative in a point and as a function
Integrationcontains 6 symbols, namely integrability and the integral over a set for Riemann, Lebesgue and Gauge-integration.
For Arithmetics we use the already existing theories from [Mitc]. It contains interfaces for below number arithmetics (each split into two interfaces for the basic number type definitions and the arithmetics on them).
Complex Numberscontains 11 symbols for complex numbers aligned to their counterparts in HOL Light, PVS and Mizar. Besides the usual arithmetic operations similar to , it contains (the imaginary unit), (the modulus of a complex number) and , (the real and imaginary parts of a complex number).
Integerscontains 9 symbols for the usual arithmetic operations on integers and for comparison between two integers.
Listscontains the 13 most important symbols for lists, including , , , and (filter a list using another list) as well as some auxiliary definitions. There are no lists in Mizar, instead finite sequences are used. These however deserve their own interface.
For Logic we use the already existing theories in the [Mita] repository. It contains 9 symbols for boolean algebra that are all perfectly aligned to HOL Light, PVS and Mizar, and sometimes also to Coq.
Setsare also already existent in [Mitc], split into many subtheories. 28 of the contained symbols have been aligned. sets contains symbols for typed sets as in a type theoretical setting, including axioms and theorems. Here we have the most alignments so far. It also contains the following two interfaces:
Functionscontains 7 symbols for alignments to functions and their relations, that are not already contained in relations.
Topologycontains 25 symbols for both general topological spaces as well as the standard topology on specifically.
In order to translate an expression from one library to another, the concepts in the expression must at least exist in both libraries. This creates the need to inspect the intersection of the concepts in these libraries. Table 15.1 gives an overview of the library intersection for various interface theories.
|
|
||||
|
Topic
|
1 System
|
2 Systems
|
3 Systems
|
4 Systems
|
|
|
||||
|
Algebra
|
17
|
9
|
5
|
0
|
|
|
||||
|
Calculus
|
35
|
7
|
8
|
0
|
|
|
||||
|
Categories
|
4
|
5
|
0
|
0
|
|
|
||||
|
Combinatorics
|
25
|
6
|
0
|
1
|
|
|
||||
|
Complex Numbers
|
10
|
5
|
3
|
3
|
|
|
||||
|
Graphs
|
72
|
6
|
3
|
0
|
|
|
||||
|
Integers
|
52
|
2
|
7
|
0
|
|
|
||||
|
Lists
|
28
|
8
|
9
|
0
|
|
|
||||
|
Logic
|
18
|
0
|
2
|
5
|
|
|
||||
|
Natural Numbers
|
53
|
2
|
10
|
2
|
|
|
||||
|
Polynomials
|
12
|
0
|
0
|
0
|
|
|
||||
|
Rational Numbers
|
11
|
4
|
2
|
7
|
|
|
||||
|
Real Numbers
|
9
|
3
|
5
|
5
|
|
|
||||
|
Relations
|
21
|
15
|
4
|
0
|
|
|
||||
|
Sets
|
56
|
10
|
9
|
10
|
|
|
||||
|
Topology
|
62
|
2
|
8
|
0
|
|
|
||||
|
Vectors
|
25
|
5
|
0
|
0
|
|
|
||||
|
Sum
|
510
|
91
|
79
|
33
|
|
|
Table 15.1: Number of Concepts Found in Exactly One, Two, Three or Four Systems
Figure 15.3 shows a small part of the theory graph of the MitM libraries. The full MitM theory graph can be explored on MathHub.
15.2Implementation
I have implemented a prototypical expression translator in the Mmt system that uses alignments, theory morphisms and programmatic tactics to translate expressions in the form of Mmt terms. The translation mechanism is already used in the OpenDreamKit project and is exposed via the Mmt query language [Rab12].
Crucially, the algorithm returns partial translations when no full translation to a target library can be found. These can be used for finding new alignments automatically by the techniques described in Chapter 16.
1.
2.
3.
We can obtain translators in several ways:
•
•
•
•
–
–
•
The Algorithm (Term,Boolean) then reduces to a simple tree search, iteratively applying applicable translators in to subterms of until is satisfied, or return a partial translation if no full translation of can be found.
This implementation is naive and potentially inefficient and should be considered prototypical, but suitably demonstrates the capabilities of the general approach.
Before we cover one example in detail, Table 15.2 lists three rather simple example translations between PVS and HOL Light. We use the Pi-types of LF to bind variables on the outside of the intended expressions.
Note that even something like the application of a function entails a translation from function application in HOL Light to function application in PVS, since they belong to their respective system dialects. Furthermore, the translation from simple function types in HOL Light to the dependent -type in PVS is actually done on the level of interface theories, where simple function types are defined as a special case of dependent function types (see Section 15.1.2). Unlike the latter two, the first example uses only primitive symbols in both systems that are not part of any external library. Meta-variables have been left out in the third example for brevity.
Furthermore, an argument alignment was used in the third example, that switches the two (non-implicit) arguments – namely the predicate and the list. Whereas this usually trips up automated translation processes or needs to be manually implemented, in our case this is as easy as adding (in this case) the key-value-pair to the alignment.
15.3Example
To exemplify the usefulness of such translations across libraries, we will examine one example with computer algebra systems – which the OpenDreamKit research community has come to call Jane’s Use Case [Koh+17a] – in detail. This example is interesting in that it was (chiefly) developed by John Cremona as a real-world situation a computational group theorist might find themself in, and where they would want to use a combination of computer algebra systems.
A user, Jane, wants to experiment with invariant theory of finite groups. She does so, by considering some group as acting on the variables of the polynomial ring and studying the ideals generated by the orbit of some polynomial, since these happen to be fixed by the group action. Naturally, in a computational setting one would want to have the Gröbner bases of these ideas as well. GAP happens to be efficient in computing orbits, whereas Singular is known to be very efficient in computing Gröbner bases. For the purposes of this section (and in light of Chapter 12) we will substitute Singular by Sage.
Starting from the Math-in-the-Middle ontology (see Section 3.4), Jane wants to study the dihedral group . So she declares a polynomial – exemplary – over , and wants to compute the orbit in GAP, translate the resulting ideal back to MitM as , declare its Gröbner base , translate this to Sage in order to compute it and have the result presented to her back in MitM.
There are two things that make this example particularly non-trivial:
1.
2.
The polynomial is formally constructed in GAP using the (internal) syntax
where represents lists, and represents the monomial . The precise meaning of the and symbols is technical and largely irrelevant.
In Sage, the same polynomial is instead constructed as
where represents the monomial . Consequently, monomials refer to the specific named variables of the polynomial ring provided as an argument.
In general and not surprisingly, there seems to be no universally agreed upon method to formally represent polynomials.
The symbols for lists, integers, Gröbner bases, ideals (which in a computational setting can be represented as a list of generators) and orbits can be easily expressed as typed constants in an interface theory and connected via alignments, so we can focus on those aspects of the translation that are non-trivial.
The discrepancy regarding dihedral groups is reflective of different notational conventions used in the mathematical community, hence it makes sense to have both of them represented in an interface. Correspondingly, for the interface theory in the Math-in-the-Middle library we use both and simply use definitions to convert between them:
Listing 15.4: An Interface Theory for Dihedral Groups
Which allows us to use simple alignments to translate from GAP/Sage to MitM and definition expansion to translate from the second to the first variant. For the other direction, we need a theory morphism, e.g. a view:
Listing 15.5: An View for Translating Dihedral Groups
Regarding converting polynomials, we are stuck with using a programmatic translator instead. For a MitM representation of polynomials, we use a more generic method that carries the names of the variables:
The polynomial would then be represented as
The only thing missing then are programmatic translators from GAP and Sage to MitM and their inverses. As an example, Listing 15.7 shows the translator from MitM polynomials to GAP polynomials, using helper objects (analogous to those described in Section 5.2.1).
Given these translators, Jane’s Use Case can be realized as a sequence of applications of the translation algorithm described in Section 15.2.
Figure 15.4 shows the realization of this use case in a Jupyter [Jup] notebook running an Mmt kernel. Here, the expression is used to instruct the Mmt system to translate the expression to the ontology of system and have the target system evaluate the expression.
Chapter 16
Viewfinding
Theory morphisms underly the notion of theory graphs. They are one of the primary structuring tools employed in Mmt and enable the kind of modularity we aimed for in this thesis, most notably Part II. As they induce new theorems in the target theory for any of the source theory, views (as opposed to includes and other trivial morphisms, see Section 4.1.1) in particular are high-value elements of a modular formal library. Usually, these are manually encoded, but this practice requires authors who are familiar with source and target theories at the same time, which limits the scalability of the manual approach.
To remedy this problem, I have developed a view finder algorithm that automates theory morphism discovery, and implemented it in Mmt. While this algorithm conceptually makes use of the definitional property of theory morphisms that they are to preserve typing judgements, it ultimately operates on the level of individual declarations after preprocessing which may include translations as in Chapter 15 using alignments – as such, it can also be thought of as an alignment finder across libraries, simultaneously utilizing and extending the set of possible translations between them.
Here, we focus on one specific application of theory classification, where a user can check whether a (part of a) formal theory already exists in some library, potentially avoiding duplication of work or suggesting an opportunity for refactoring.
The basic use case is the following: Mary, a mathematician, becomes interested in a class of mathematical objects, say – as a didactic example – something she initially calls “beautiful subsets” of a base set (or just “beautiful over ”). These have the following properties :
1.
the empty set is beautiful over 2.
every subset of a beautiful set is beautiful over 3.
If and are beautiful over and has more elements than , then there is an , such that is beautiful over . To see what is known about beautiful subsets, she types these three conditions into a theory classifier, which computes any theories in a library that match these (after a suitable renaming). In our case, Mary learns that her “beautiful sets” correspond to the well-known structure of matroids [MWP], so she can directly apply matroid theory to her problems.
In extended use cases, a theory classifier may find theories that share significant structure with , so that Mary can formalize modularly with minimal effort. Say Mary was interested in “dazzling subsets”, i.e. beautiful subsets that obey a fourth condition, then she could just contribute a theory that extends the theory by a formalization of the fourth condition – and maybe rethink the name.
Existing systems have so far only worked with explicitly given views, e.g., in IMPS [FGT93] or Isabelle [Isa]. Automatically and systematically searching for new views was first undertaken in [NK07] in 2006. However, at that time no large corpora of formalized mathematics were available in standardized formats that would have allowed easily testing the ideas in practice.
This situation has changed since then as multiple such exports have become available. In particular, we now have OMDoc/Mmt as a uniform representation language for such corpora. Building on these developments, we are now able, for the first time, to apply generic methods — i.e., methods that work at the Mmt level — to search for views in formal libraries.
While inspired by the ideas of [NK07], the design and implementation presented here are completely novel. In particular, the theory makes use of the rigorous language-independent definitions of theory and view provided by Mmt.
[GK14a] applies techniques related to ours to a related problem. Instead of views inside a single corpus, they use machine learning to find similar constants in two different corpora. Their results can roughly be seen as a single partial view from one corpus to the other.
16.1The Viewfinder Algorithm
Let be a corpus of theories with (for now) the same fixed meta-theory . We call the problem of finding views between theories of the view finding problem and an algorithm that solves it a view finder. Note that a view finder is sufficient to solve the theory classification use case above: Mary provides a -theory of beautiful sets, the view finder computes all (total) views from into .
Efficiency ConsiderationsThe cost of this problem quickly explodes. First of all, it is advisable to restrict attention to simple views (see Section 4.1.1). Eventually we want to search for arbitrary views as well. But that problem is massively harder because it subsumes theorem proving: a view from to maps -axioms to -proofs, i.e., searching for a view requires searching for proofs.
Secondly, if has theories, we have pairs of theories between which to search. (It is exactly because the direction matters, and even views from a theory to itself are interesting.) Moreover, for two theories with and constants, there are possible simple views (It is exactly because views may map different constants to the same one.) Thus, we can in principle enumerate and check all possible simple views in . But for large , it quickly becomes important to do so in an efficient way that eliminates ill-typed or uninteresting views early on.
Thirdly, it is desirable to search for partial views as well. In fact, identifying refactoring potential in libraries is only possible if we find partial views: then we can refactor the involved theories in a way that yields a total view (see Chapter 17). Moreover, many proof assistant libraries do not follow the little theories paradigm or do not employ any theory-like structuring mechanism at all. These can only be represented as a single huge theory, in which case we have to search for partial views from this theory to itself – facilitating the aforementioned refactoring technique. While partial views can be reduced to and then checked like total ones, searching for partial views makes the number of possible views that must be checked much larger.
Finally, even for a simple view, checking reduces to a set of equality constraints, namely the constraints for the type-preservation condition (see Section 4.1.1). Depending on , this equality judgment may be undecidable and require theorem proving.
A central motivation for my algorithm is that equality in can be soundly approximated very efficiently by using a normalization function on -expressions. This has the additional benefit that relatively little meta-theory-specific knowledge is needed, and all such knowledge is encapsulated in a single well-understood function. This way we can implement view–search generically for arbitrary .
The algorithm consists of two steps. First, we preprocess all constant declarations in with the goal of moving as much intelligence as possible into a step whose cost is linear in the size of . Then, we perform the view search on the optimized data structures produced by the first step.
16.1.1Preprocessing
The preprocessing phase computes for every constant declaration a normal form and then efficiently stores the abstract syntax tree (defined below) of . Both steps are described below.
Normalizationinvolves two steps: Mmt-level normalization performs generic transformations that do not depend on the meta-theory . These include flattening and definition expansion. Importantly, we do not fully eliminate defined constant declarations from a theory : instead, we replace them with primitive constants and replace every occurrence of in other declarations with . If is the domain theory, we can simply ignore (because views do not have to provide an assignment to defined constants). But if the is the codomain theory, retaining increases the number of views we can find; in particular in situations where is a type of proofs, and hence a theorem.
Meta-theory-level normalization applies an -specific normalization function. In general, we assume this normalization to be given as a black box. However, because many practically important normalization steps are widely reusable, we provide a few building blocks, from which specific normalization functions can be composed. Skipping the details, these include:
1.
Top-level universal quantifiers and implications are rewritten into the function space of the logical framework using the Curry-Howard correspondence. 2.
The order of curried domains of function types is normalized as follows: first all dependent argument types are ordered by the first occurrence of the bound variables; then all non-dependent argument types are ordered by the abstract syntax tree of . 3.
Implicit arguments, whose value is determined by the values of the others are dropped, e.g. the type argument of an equality. This has the additional benefit of shrinking the abstract syntax trees and speeding up the search. 4.
Equalities are normalized such that the left hand side has a smaller abstract syntax tree. Above multiple normalization steps make use of a total order on abstract syntax trees. We omit the details and only remark that we try to avoid using the names of constants in the definition of the order — otherwise, declarations that could be matched by a view would be normalized differently. Even when breaking ties between requires comparing two constants, we can first try to recursively compare the syntax trees of their types.
Abstract Syntax TreesWe define abstract syntax trees as pairs where is subject to the grammar
(where is a non-terminal for natural numbers) and is a list of constant names.
We obtain an abstract syntax tree from an MMT expression by (i) switching to de-Bruijn representation of bound variables and (ii) replacing all occurrences of constants with in such a way that every refers to the -th element of .
Abstract syntax trees have the nice property that they commute with the application of simple views : If represents , then is represented by where arises from by replacing every constant with its -assignment.
The above does not completely specify and yet, and there are several possible canonical choices among the abstract syntax trees representing the same expression. The trade-off is subtle because we want to make it easy to both identify and check views later on. We call the long abstract syntax tree for if replaces the -th occurrence of a constant in when is read in left-to-right order. In particular, the long tree does not merge duplicate occurrences of the same constant into the same number. The short abstract syntax tree for arises from the long one by removing all duplicates from and replacing the accordingly.
For our algorithm, we pick the long abstract syntax tree, which may appear surprising. The reason is that shortness is not preserved when applying a simple view: whenever a view maps two different constants to the same constant, the resulting tree is not short anymore. Length, on the other hand, is preserved. The disadvantage that long trees take more time to traverse is outweighed by the advantage that we never have to renormalize the trees.
16.1.2Search
Consider two constants and , where and are preprocessed into long abstract syntax trees and . It is now straightforward to show the following Lemma:
Proof.The claim is simply the typing-preservation condition of theory morphisms for the special case of simple views; expressed using abstract syntax trees.
Of course, the condition about may be redundant if contains duplicates; but because has to be traversed anyway, it is cheap to skip all duplicates. We call the set of assignments the prerequisites of .
Proof.Note that the algorithm constructs a partial view by recursively ensuring that the premises of Theorem 16.1 holds.
To find all views from to , we first run the core algorithm on every pair of -constants and -constants. This usually does not yield big views yet. For example, consider the typical case where theories contain some symbol declarations and some axioms, in which the symbols occur. Then the core algorithm will only find views that map at most one axiom.
Depending on what we intend to do with the results, we might prefer to consider them individually (e.g. to yield alignments). But we can also use these small views as building blocks to construct larger, possibly total ones:
Proof.Note that it is sufficient to show that for any constant in its domain, the amalgamated view satisfies . Since the partial views amalgamated to are assumed to be compatible and well-typed, this immediately follows from the assignment being in (at least) one of the constituent partial views.
16.1.3Optimizations
The above presentation is intentionally simple to convey the general idea. We now consider a few advanced features of the implementation to enhance scalability.
Caching Preprocessing ResultsBecause the preprocessing performs normalization, it can be time-consuming. Therefore, we allow for storing the preprocessing results to disk and reloading them in a later run.
Fixing the Meta-TheoryWe improve the preprocessing in a way that exploits the common meta-theory, which is meant to be fixed by every view. All we have to do is, when building the abstract syntax trees , to retain all references to constants of the meta-theory in instead of replacing them with numbers. With this change, will never contain meta-theory constants, and the core algorithm will only find views that fix all meta-theory constants. Because is much shorter now, the view search is much faster.
It is worth pointing out that the meta-theory is not always as fixed as one might think. Often we want to consider certain constants, that are defined early on in the library and then used widely, to be part of the meta-theory. In PVS (see Chapter 10), this makes sense, e.g., for all operations defined in the Prelude library. For across-library view finding, we might also apply a partial translation (in the sense of Chapter 15) to the target library first and consider all succesfully translated symbols as part of the meta-theory, ensuring that all morphisms found are compatible with and predicated on already known alignments and morphisms.
Note that we still only have to cache one set of preprocessing results for each library: changes to the meta-theory only require minor adjustments to the abstract syntax trees without redoing the entire normalization.
Biasing the Core AlgorithmThe core algorithm starts with an assignment and then recurses into constant that occur in the declarations of and . This occurs-in relation typically splits the constants into layers. A typical theory declares types, which then occur in the declarations of function symbols, which then occur in axioms. Because views that only map type and function symbols are rarely interesting (because they do not allow transporting non-trivial theorems), we always start with assignments where is an axiom, but other conditions for starting declarations are possible.
Exploiting Theory StructureLibraries are usually highly structured using imports between theories. If is imported into , then the set of partial views out of is a superset of the set of partial views out of . If implemented naively, that would yield a quadratic blow-up in the number of views to consider.
Instead, when running our algorithm on an entire library, we only consider views between theories that are not imported into other theories. In an additional postprocessing phase, the domain and codomain of each found partial view are adjusted to the minimal theories that make well-typed.
16.2Implementation
I have implemented our view finder algorithm in the Mmt system and exposed it in Mmt’s jEdit IDE. A screenshot of Jane’s theory of beautiful sets is given in Figure 16.1. Right-clicking anywhere within the theory allows Jane to select . The latter menu offers a choice of known libraries in which the view finder should look for codomain theories; is the Math-in-the-Middle library (see Section 3.4).
After choosing , the view finder finds two views (within less than one second) and shows them (Figure 16.2).
The first of these () has a theory for matroids as its codomain, which is given in Listing 16.1. Inspecting that theory and the assignments in the view, we see that it indeed represents the well-known correspondence between beautiful sets and matroids.
The latter uses predefined propositions in its axioms and uses a type for the collection of sets, while the former has the statements of the axioms directly in the theory and uses a predicate – since (typed) sets are defined as predicates, definition expansion is required for matching. Additionally, the implication that beautiful sets (or sets in a matroid) are finite is stated as a logical formula in the former, while the latter uses the Curry/Howard correspondence.
16.3Cross-Library Viewfinding
We now generalize view finding to the situation where domain and codomain live in different libraries written in different logics. Intuitively, the key idea is that we now have two fixed meta-theories and and a fixed meta-view . However, due to the various idiosyncrasies of logics, tools’ library structuring features and individual library conventions, this problem is significantly more difficult than intra-library view finding. For example, unless the logics are closely related, meta-views usually do not even exist and must be approximated. Therefore, a lot of tweaking is typically necessary, and it is possible that multiple runs with different trade-offs give different interesting results.
As an example, we present a large case study where we find views from the MitM library used in the running example so far into the PVS/NASA library (see Chapter 10).
Theory Structure NormalizationPVS’s complex and prevalently used parametric theories critically affect view finding because they affect the structure of theories. For example, the theory of groups in the NASA library has three theory parameters for the signature of groups, includes the theory with the same parameters, and then declares the axioms for a group in terms of these parameters. Without special treatment, we could only find views from/into libraries that use the same theory structure.
We have investigated three approaches of handling parametric theories:
1.
Simple treatment: We drop theory parameters and interpret references to them as free variables that match anything. This is of course not sound so that all found views must be double-checked. However, because practical search problems often do not require exact results, even returning all potential views can be useful. 2.
Covariant elimination: We treat theory parameters as if they were constants declared in the body. In the above mentioned theory 3.
Contravariant elimination: The theory parameters are treated as if they were bound separately for every constant in the body of the theory. In the above mentioned theory I have implemented the first two approaches. The first is the most straightforward but it leads to many false positives and false negatives. I have found the second approach to be the most useful for inter-library search since it most closely corresponds to simple formalizations of abstract theories in other libraries. The third approach will be our method of choice when investigating intra-library views of PVS/NASA in future work.
As a first use case, we can write down a theory for a commutative binary operator using the MitM foundation, while targeting the PVS Prelude library – allowing us to find all commutative operators, as in Figure 16.3 (using the simple approach to theory parameters).
This example also hints at a way to iteratively improve the results of the view finder: since we can find properties like commutativity and associativity, we can use the results to in turn inform a better normalization of the theory by exploiting these properties. This in turn would potentially allow for finding more views.
To evaluate the approaches to theory parameters we used a simple theory of monoids in the MitM foundation and the theory of monoids in the NASA library as domains for viewfinding with the whole NASA library as target using simple and covariant approaches. The results are summarized in Figure 16.4.
Most of the results in the simple MitMNASA case are artifacts of the theory parameter treatment and view amalgamation – in fact only two of the 17 results are meaningful (to operations on sets and the theory of number fields). In the covariant case, the additional requirements lead to fuller (one total) and less spurious views. With a theory from the NASA library as domain, the results are already too many to be properly evaluated by hand. With the simple approach to theory parameters, most results can be considered artifacts; in the covariant case, the most promising results yield (partial) views into the theories of semigroups, rings (both the multiplicative and additive parts) and most extensions thereof (due to the duplication of theory parameters as constants).
16.4Applications for Viewfinding
We have seen how a view finder can be used for theory classification and finding constants with specific desired properties, but many other potential use cases are imaginable. The main problems to solve with respect to these is less about the algorithm or software design challenges, but user interfaces.
The theory classification use case described in Section 16.2 is mostly desirable in a setting where a user is actively writing or editing a theory, so the integration in jEdit is sensible. However, the across-library use case in Section 16.3 already would be a lot more useful in a theory exploration setting, such as when browsing available archives on MathHub [Ian+14] or in the graph viewer integrated in Mmt [RKM17]. Additional specialized user interfaces would enable or improve the following use cases:
•
Furthermore, partial views – especially those that are total on some included theory – could be insightful counterexamples.
•
Additionally, surjective partial views would inform her, that her theory would probably better be refactored as an extension of the codomain, which would allow her to use all theorems and definitions therein.
•
•
This would allow for e.g. discovering and importing theorems and useful definitions from some other library – which on the basis of our encodings can be done directly by the view finder.
A useful interface might specifically prioritize views into theories on top of which there are many theorems and definitions that have been discovered.
For some of these use cases it would be advantageous to look for views into our working theory instead.
Note that even though the algorithm is in principle symmetric, some aspects often depend on the direction – e.g. how we preprocess the theories, which constants we use as starting points or how we aggregate and evaluate the resulting (partial) views (see Sections 16.1.3 and 16.3).
Chapter 17
Refactoring and Theory Discovery via Theory Intersections
An important driver of mathematical development is the discovery of new mathematical objects, concepts and theories. Even though there are many different situations that give rise to a new theory, it seems that a common instance is the discovery of commonalities between apparently different mathematical structures (if such exist). In fact, many of the algebraic theories in Bourbaki naturally arise as the “common part” of two (or more) different mathematical structures – for instance, one could interpret the theory of groups as the common theory of and the set of symmetrical operations on e.g. a square.
In [Koh14], Kohlhase proposes a notion of theory intersection – elaborating an earlier formalization from [Nor08] to Mmt [RK13b; HKR12b] that captures this phenomenon in a formal setting: Let two theories and , a partial view with domain and codomain , and its partial inverse (as in Figure 17.1 on the left) be given. Then we can pass to a more modular theory graph, where and (as in Figure 17.1 on the right). In this case we think of the isomorphic theories and as the intersection of theories and along and .
17.1Theory Intersection by Example
To fortify our intuitions, we examine a concrete mathematical example in detail.
We start out with a theory of positive natural numbers with addition and intersect it with of strings with concatenation (as in Figure 17.2). Note that we do not start with modular developments; rather the modular structure is (going to be) the result of intersecting with various examples. Also, note that the views k and l are both partial.
Now the intersection as proposed above yields Figure 17.3, which directly corresponds to the schema in Figure 17.1. Note, that the new pair of (equivalent) theories is completely determined by the partial morphism ; the only thing we have to invent are the names – and we have not been very inventive here.
Intuitively, the intersection theory is the theory of semigroups which is traditionally written down in Mmt as in Figure 17.4. And indeed, is a renaming of both and .
For this situation, we should have a variant theory intersection operator that takes a partial morphism and returns one intersection theory.
In this situation, we want a theory intersection operator that follows the schema in Figure 17.5.
Let us call this operation unary TI and the previous one binary TI. To compute it, we need to specify a name for the new theory and two renamings and . Note that in this TI operator, the intersection is connected to the “rest theories” via Mmt structures – rather than mere inclusions – which carry the assignments induced by the partial morphisms suitably composed with the renamings (see next section).
In our example we can obtain the theory from Figure 17.4 via the renamings and .
Unary TI is often the more useful operation on theory graphs, but needs direct user supervision, whereas binary TI is fully automatic if we accept generated names for the intersection theories.
17.2Reducing Partial Morphisms to Renamings
In the previous example it is noteworthy, that the morphisms k and l are fully inverse to each other. In fact, they are renamings. By a renaming, we mean a partial morphism such, that for every constant declared in , is again a constant (as opposed to a complex term).
Naturally, theory intersections are a lot simpler for renamings. In fact, we only need a single renaming to intersect along (since the inverse of a renaming is again a renaming and uniquely determined). It turns out, that we can always reduce the situation in Figure 17.1 to the much easier case, where we have a single renaming , where and are conservative extensions of our original theories:
Let be a partial theory morphism and for a complex term . We can then conservatively extend to a theory that contains a new defined constant and adapt to a new morphism with (and ), as in Figure 17.6. If we repeat this process for every mapping that is not already a simple renaming, we yield a new conservative extension such, that the corresponding morphism (accordingly adapted) is a renaming.
Doing the same with a partial inverse , we ultimately get a single renaming that is equivalent to the original pair of partial morphisms. We can therefore w.l.o.g. reduce ourselves in every instance to this case.
17.3Implementation
I have implemented a method for unary TI in an earlier version of the Mmt API.
The intersection method takes as parameters two theories, a name for the intersection and a list of pairs of declarations, which can be obtained from a pair of morphisms, a single morphism or use the view finder presented in Chapter 16. It returns the intersection theory and the refactored versions of (conservative extensions of) the original theories, depending on the original morphisms provided.
Both methods are integrated into a refactoring panel, which is part of the Mmt plugin for jEdit. To intersect two theories, the user can either provide one or two morphisms between the theories or allow the Viewfinder to pick for them. The declarations in the intersection theory can optionally be named.
An annotated video demonstration of the refactoring panel and its components can be found on Youtube [IntV15].
If we accept automatically generated names for the theory intersections, we can eliminate user interaction and use the view finder to automate the intersection operation on a set of theories without having to provide the morphisms to intersect along beforehand. This could be used to refactor whole libraries in a more modular way (in concordance with the little theories approach [FGT92b]). Additionally, by supplying the view finder with alignments and other translators between libraries, our approach could be used to refactor a whole library along the theory graph of an already modular library.
We do not yet have a heuristic to evaluate (the resulting) theories automatically with respect to their interest; however, given a morphism between two interesting theories, we have observed that the corresponding intersection tends to be interesting as well, as long as the morphism is not meaningless itself.
Figure 17.3: Positive Integers and Strings, Refactored
Figure 17.4: Semigroups
Figure 17.5: Unary TI
Figure 17.6: Obtaining a Renaming From a Morphism
Part V
Conclusion and Future Work
We have seen how we can take on the integration problem for formal libraries by representing them in a unifying meta-framework (Part III), using a flexible logical framework to specify their foundations (Part II), aligning their contents (Chapter 14) and implementing foundation-independent alignment-aware algorithms for identifying overlap (Chapter 16) suggestive of new alignments, translating expressions across libraries (Chapter 15) and modularize library content by refactoring along theory intersections (Chapter 17).
The knowledge management techniques described in Part IV are certainly not exhaustive; many more services are imaginable, but the ones presented in this thesis demonstrate the effectiveness of the general approach to library integration described herein. Furthermore, these facilitate the aims of the OAF (see Section 3.5) and OpenDreamKit (see Section 3.3 ) projects, as demonstrated in Section 15.3. Additionally they represent steps towards a system integrating all aspects of the tetrapod (see Chapter 1); demonstrably inference, computation, tabulation and organization.
Naturally, this opens up many avenues for future research and improvements, which fall broadly into three categories:
1. FundamentalsMany implementations described in this thesis are prototypical and can be optimized or otherwise improved. In particular:
1.
2.
3.
4.
To check a judgement we have two strategies: We can either simplify until we find an applicable foundation-dependent typing rule specifically for (the head symbol of) , or we can try to infer the principal type of and check . In most cases, the existence of a typing rule implies that the former strategy will quickly yield a result, whereas inferring the type can be expensive, and hence the former strategy is attempted first. However, imagine being a single reference to a constant with a complex definiens, and being a function application , where the return type of is . In this case, inferring the principal type of is fast and the subsequent check trivial, whereas simplifying leads to definition expansion and subsequent further simplifications, which will ultimately need to be repeated for the inferred type of as well, since a function application can only ever check against any type via the inference strategy. This kind of situation seems to occur regularly in high-level formalizations, and is correspondingly often encountered in the development of the Math-in-the-Middle library.
To remedy this problem, I am currently actively working on a reimplementation of the Mmt solver algorithm using multithreading; not just to exploit multicore processors, but to be able to compute conflicting checking strategies on separate threads in parallel, such that if either strategy terminates quickly, the checking algorithm can return a result just as quickly. This would obviate the current advantage of being cautious with adding potentially slow inference rules.
2. Scaling UpMany of the implementations and approaches presented in this thesis scale in usefulness and coverage depending on a certain amount of available data, features and implementations. All of these can and should be scaled up in the future, such as:
1.
2.
3.
4.
5.
6.
3. WorkflowsOne of the major obstacles in using all of the techniques in this thesis is a certain lack of tool support with respect to specific workflows for various use cases. Especially the algorithms presented in Part IV are primarily usable by programmatically calling methods in the Mmt API, or via commands in the Mmt shell. Exemplary, in Chapter 16 my coauthors and I (on the original publication) already conjecture on possible applications for the view finder algorithm, most of which are predicated on the existence of a bespoke user interface for that particular use case. Designing such interfaces entails thinking deeply about realistic and convenient workflows for different situations and users.
This also applies to Mmt’s surface syntax, which requires a very reasonable, but (for example, for working mathematicians not familiar with formal systems) potentially prohibitive amount of time and effort to get accustomed to.
I have written an Mmt plugin for IntelliJ IDEA, a java-based IDE which offers a rich plugin API, to experiment with integrating various generic services in a more flexible IDE than the only previously supported one, jEdit. In the future, I would like to investigate the possibility of using e.g. sT
E
X [Koh08] or possibly even plain L
A
T
E
X as an alternative input language for formal Mmt content, as well as designing a unifying online IDE on MathHub for working with Mmt and its connected systems and libraries, obviating the need to set up and use Mmt (and the multitude of systems with which Mmt can interact) locally – a process which (even using docker images, jupyter notebooks and similar solutions) can be prohibitively complicated for non-experts, especially when lacking a unifying user interface. Chapter 18
Bibliography
[Con+]
A. Condoluci, M. Kohlhase, D. Müller, F. Rabe, C. S. Coen, and M. Wenzel. “Relational Data Across Mathematical Libraries”. Accepted for CICM 2019. url: .[Deh+16]
P.-O. Dehaye et al.. “Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach”. in: Intelligent Computer Mathematics 2016. Conferences on Intelligent Computer Mathematics (Bialystok, Poland, July 25–29, 2016). ed. by M. Kohlhase, M. Johansson, B. Miller, L. de Moura, and F. Tompa. LNAI 9791. Springer, 2016. url: .[Kal+16]
C. Kaliszyk, M. Kohlhase, D. Müller, and F. Rabe. “A Standard for Aligning Mathematical Concepts”. in: Work in Progress at CICM 2016. ed. by A. Kohlhase, M. Kohlhase, P. Libbrecht, B. Miller, F. Tompa, A. Naummowicz, W. Neuper, P. Quaresma, and M. Suda. CEUR-WS.org, 2016, 229–244.[Koh+17a]
M. Kohlhase, D. Müller, M. Pfeiffer, F. Rabe, N. Thiéry, V. Vasilyev, and T. Wiesing. “Knowledge-Based Interoperability for Mathematical Software Systems”. in: Mathematical Aspects of Computer and Information Sciences. ed. by J. Blömer, I. Kotsireas, T. Kutsia, and D. Simos. Springer, 2017, 195–210.[Koh+17b]
M. Kohlhase, T. Koprucki, D. Müller, and K. Tabelow. “Mathematical models as research data via flexiformal theory graphs”. in: Intelligent Computer Mathematics (CICM) 2017. Conferences on Intelligent Computer Mathematics. ed. by H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke. LNAI 10383. Springer, 2017. doi: . url: .[Koh+17c]
M. Kohlhase, D. Müller, S. Owre, and F. Rabe. “Making PVS Accessible to Generic Services by Interpretation in a Universal Format”. in: Interactive Theorem Proving. ed. by M. Ayala-Rincón and C. A. Muñoz. vol. 10499. LNCS. Springer, 2017. url: .[Kop+18]
T. Koprucki, M. Kohlhase, K. Tabelow, D. Müller, and F. Rabe. “Model pathway diagrams for the representation of mathematical models”. in: Journal of Optical and Quantum Electronics 50.2 (2018), 70. doi: .[MK15]
D. Müller and M. Kohlhase. “Understanding Mathematical Theory Formation via Theory Intersections in MMT”. 2015. url: .[MKR18]
D. Müller, M. Kohlhase, and F. Rabe. “Automatically Finding Theory Morphisms for Knowledge Management”. in: Intelligent Computer Mathematics (CICM) 2018. Conferences on Intelligent Computer Mathematics. ed. by F. Rabe, W. Farmer, A. Youssef, and .... LNAI. in press. Springer, 2018. url: .[MR19]
D. Müller and F. Rabe. “Rapid Prototyping Formal Systems in MMT: 5 Case Studies”. Accepted for LFMTP 2019. 2019. url: .[MRK18]
D. Müller, F. Rabe, and M. Kohlhase. “Theories as Types”. in: ed. by D. Galmiche, S. Schulz, and R. Sebastiani. Springer Verlag, 2018. url: .[MRS]
D. Müller, F. Rabe, and C. Sacerdoti Coen. “The Coq Library as a Theory Graph”. Submitted to CICM 2019. url: .[Mül+17a]
D. Müller, C. Rothgang, Y. Liu, and F. Rabe. “Alignment-based Translations Across Formal Systems Using Interface Theories”. in: Proof eXchange for Theorem Proving. ed. by C. Dubois and B. Woltzenlogel Paleo. Open Publishing Association, 2017, 77–93.[Mül+17b]
D. Müller, T. Gauthier, C. Kaliszyk, M. Kohlhase, and F. Rabe. “Classification of Alignments between Concepts of Formal Mathematical Systems”. in: Intelligent Computer Mathematics (CICM) 2017. Conferences on Intelligent Computer Mathematics. ed. by H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke. LNAI 10383. Springer, 2017. doi: . url: .[Mül+17c]
D. Müller, T. Gauthier, C. Kaliszyk, M. Kohlhase, and F. Rabe. Classification of Alignments between Concepts of Formal Mathematical Systems. tech. rep.. 2017. url: (visited on 05/21/2017).[RKM16]
D. Rochau, M. Kohlhase, and D. Müller. “FrameIT Reloaded: Serious Math Games from Modular Math Ontologies”. in: Intelligent Computer Mathematics – Work in Progress Papers. ed. by M. Kohlhase, A. Kohlhase, P. Libbrecht, B. Miller, A. Naumowicz, W. Neuper, P. Quaresma, F. Tompa, and M. Suda. 2016. url: .[Asp+06a]
A. Asperti, C. S. Coen, E. Tassi, and S. Zacchiroli. “Crafting a Proof Assistant”. in: TYPES. ed. by T. Altenkirch and C. McBride. Springer, 2006, 18–32.[Aus+03]
R. Ausbrooks et al.. “Mathematical Markup Language (MathML) v. 2.0.”. in: World Wide Web Consortium recommendation (2003).[BCH12]
M. Boespflug, Q. Carbonneaux, and O. Hermant. “The -calculus modulo as a universal proof language”. in: Proceedings of PxTP2012: Proof Exchange for Theorem Proving. ed. by D. Pichardie and T. Weber. 2012, 28–43.[Bra13]
E. Brady. “Idris, a general-purpose dependently typed programming language: Design and implementation”. in: Journal of Functional Programming 23.5 (2013), 552–593.[Bus+04]
S. Buswell, O. Caprotti, D. P. Carlisle, M. C. Dewar, M. Gaetano, and M. Kohlhase. The Open Math standard. tech. rep.. version 2.0. The Open Math Society, 2004.[Con+86]
R. Constable et al.. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, 1986.[Coq15]
Coq Development Team. The Coq Proof Assistant: Reference Manual. tech. rep.. INRIA, 2015.[Dun+15]
C. Dunchev, F. Guidi, C. S. Coen, and E. Tassi. “ELPI: Fast, Embeddable, lambda-Prolog Interpreter”. in: Logic for Programming, Artificial Intelligence, and Reasoning. ed. by M. Davis, A. Fehnker, A. McIver, and A. Voronkov. 2015, 460–468.[FGT]
W. M. Farmer, J. Guttman, and J. Thayer. The IMPS online theory library. url: (visited on 12/17/2014).[FGT93]
W. Farmer, J. Guttman, and F. Thayer. “IMPS: An Interactive Mathematical Proof System”. in: Journal of Automated Reasoning 11.2 (1993), 213–248.[GC14]
D. Ginev and J. Corneli. “NNexus Reloaded”. in: Intelligent Computer Mathematics 2014. Conferences on Intelligent Computer Mathematics (Coimbra, Portugal, July 7–11, 2014). ed. by S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban. LNCS 8543. Springer, 2014, 423–426. url: .[Gog+93]
J. Goguen, T. Winkler, J. Meseguer, K. Futatsugi, and J. Jouannaud. “Introducing OBJ”. in: Applications of Algebraic Specification using OBJ. ed. by J. Goguen, D. Coleman, and R. Gallimore. Cambridge, 1993.[Gro16]
T. G. Group. GAP – Groups, Algorithms, and Programming. . [Online; accessed 30 August 2016]. 2016. url: .[Har96]
J. Harrison. “HOL Light: A Tutorial Introduction”. in: Proceedings of the First International Conference on Formal Methods in Computer-Aided Design. Springer, 1996, 265–269.[HHP93a]
R. Harper, F. Honsell, and G. Plotkin. “A framework for defining logics”. in: Journal of the Association for Computing Machinery 40.1 (1993), 143–184.[Hur09]
J. Hurd. “OpenTheory: Package Management for Higher Order Logic Theories”. in: Programming Languages for Mechanized Mathematics Systems. ed. by G. D. Reis and L. Théry. ACM, 2009, 31–37.[KMM00]
M. Kaufmann, P. Manolios, and J Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, 2000.[LMF]
T. LMFDB Collaboration. The L-functions and Modular Forms Database. . [Online; accessed 27 August 2016].[LN12]
F. Lübeck and M. Neunhöffer. GAPDoc, A Meta Package for GAP Documentation, Version 1.5.1. 2012. url: .[Mil+97]
R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML, Revised edition. MIT Press, 1997.[MN86]
D. Miller and G. Nadathur. “Higher-order logic programming”. in: Proceedings of the Third International Conference on Logic Programming. ed. by E. Shapiro. Springer, 1986, 448–462.[NPW02]
T. Nipkow, L. Paulson, and M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer, 2002.[ODK]
OpenDreamKit Open Digital Research Environment Toolkit for the Advancement of Mathematics. url: (visited on 05/21/2015).[ORS92]
S. Owre, J. Rushby, and N. Shankar. “PVS: A Prototype Verification System”. in: 11th International Conference on Automated Deduction (CADE). ed. by D. Kapur. Springer, 1992, 748–752.[PC93]
L. Paulson and M. Coen. Zermelo-Fraenkel Set Theory. Isabelle distribution, ZF/ZF.thy. 1993.[PS99]
F. Pfenning and C. Schürmann. “System Description: Twelf - A Meta-Logical Framework for Deductive Systems”. in: Automated Deduction. ed. by H. Ganzinger. 1999, 202–206.[Ran04]
A. Ranta. “Grammatical Framework — A Type-Theoretical Grammar Formalism”. in: Journal of Functional Programming 14.2 (2004), 145–189.[RK13a]
F. Rabe and M. Kohlhase. “A Scalable Module System”. in: Information and Computation 230.1 (2013), 1–54.[Sut09]
G. Sutcliffe. “The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0”. in: Journal of Automated Reasoning 43.4 (2009), 337–362.[SW83]
D. Sannella and M. Wirsing. “A Kernel Language for Algebraic Specification and Implementation”. in: Fundamentals of Computation Theory. ed. by M. Karpinski. Springer, 1983, 413–427.[Tea03]
T. C. D. Team. The Coq proof assistant reference manual (version 7.4). tech. rep.. INRIA, Rocquencourt, France, 2003.[WPN08]
M. Wenzel, L. C. Paulson, and T. Nipkow. “The Isabelle Framework”. in: Theorem Proving in Higher Order Logics (TPHOLs 2008). ed. by A. Mohamed, Munoz, and Tahar. LNCS 5170. Springer, 2008, 33–38.[AH15]
S. Autexier and D. Hutter. “Structure Formation in Large Theories”. in: Intelligent Computer Mathematics 2015. Conferences on Intelligent Computer Mathematics (Washington DC, USA, July 13–17, 2015). ed. by M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, and V. Sorge. LNCS 9150. Springer, 2015, 155–170.[Asp+06b]
A. Asperti, F. Guidi, C. S. Coen, E. Tassi, and S. Zacchiroli. “A Content Based Mathematical Search Engine: Whelp”. in: Types for Proofs and Programs, International Workshop, TYPES 2004, revised selected papers. ed. by J.-C. Filliâtre, C. Paulin-Mohring, and B. Werner. LNCS 3839. Springer Verlag, 2006, 17–32.[Bet18]
J. Betzendahl. “Translating the IMPS Theory Library to MMT / OMDoc”. Master’s Thesis. Informatik, Universität Bielefeld, Apr. 2018. url: .[BKR]
K. Berčič, M. Kohlhase, and F. Rabe. “Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation”. submitted to CICM 2019. url: .[BL]
T. Breuer and S. Linton. “The GAP 4 Type System: Organising Algebraic Algorithms”. in: Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation. ISSAC ’98. ACM, 38–45.[Bla+14]
J. C. Blanchette et al.. “Truly Modular (Co)datatypes for Isabelle/HOL”. in: ITP. ed. by G. Klein and R. Gamboa. vol. 8558. LNCS. Springer, 2014, 93–110. doi: .[Bob+11]
F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich. “Why3: Shepherd Your Herd of Provers”. in: Boogie 2011: First International Workshop on Intermediate Verification Languages. 2011, 53–64.[Bou64]
N. Bourbaki. “Univers”. in: Séminaire de Géométrie Algébrique du Bois Marie - Théorie des topos et cohomologie étale des schémas. Springer, 1964, 185–217.[Car+19]
J. Carette, W. M. Farmer, M. Kohlhase, and F. Rabe. “Big Math and the One-Brain Barrier – A Position Paper and Architecture Proposal”. submitted to Mathematical Intelligencer. 2019. url: .[CF58]
H. Curry and R. Feys. Combinatory Logic. Amsterdam: North-Holland, 1958.[CH88]
T. Coquand and G. Huet. “The Calculus of Constructions”. in: Information and Computation 76.2/3 (1988), 95–120.[Chu40]
A. Church. “A Formulation of the Simple Theory of Types”. in: Journal of Symbolic Logic 5.1 (1940), 56–68.[Cod+11]
M. Codescu, F. Horozal, M. Kohlhase, T. Mossakowski, and F. Rabe. “Project Abstract: Logic Atlas and Integrator (LATIN)”. in: Intelligent Computer Mathematics. ed. by J. Davenport, W. Farmer, F. Rabe, and J. Urban. Springer, 2011, 289–291.[Dyb97]
P. Dybjer. “Representing Inductively Defined Sets by Wellorderings in Martin-LÖF’s Type Theory”. in: Theor. Comput. Sci. 176.1-2 (Apr. 1997), 329–335. doi: . url: .[ESC07]
J. Euzenat, P. Shvaiko, and E. Corporation. Ontology matching. Springer, 2007.[FGT92a]
W. Farmer, J. Guttman, and F. Thayer. “Little Theories”. in: Conference on Automated Deduction. ed. by D. Kapur. 1992, 467–581.[FGT92b]
W. M. Farmer, J. Guttman, and J. Thayer. “Little Theories”. in: Proceedings of the 11 Conference on Automated Deduction. ed. by D. Kapur. LNCS 607. Saratoga Springs, NY, USA: Springer Verlag, 1992, 467–581.[Geu+17]
H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, eds.. Intelligent Computer Mathematics. Conferences on Intelligent Computer Mathematics. LNAI 10383. Springer, 2017. doi: .[Gin+16]
D. Ginev et al.. “The SMGloM Project and System. Towards a Terminology and Ontology for Mathematics”. in: Mathematical Software - ICMS 2016 - 5th International Congress. ed. by G.-M. Greuel, T. Koch, P. Paule, and A. Sommese. vol. 9725. LNCS. Springer, 2016. doi: . url: .[GK14a]
T. Gauthier and C. Kaliszyk. “Matching concepts across HOL libraries”. in: Intelligent Computer Mathematics. ed. by S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban. Springer, 2014, 267–281.[GK14b]
T. Gauthier and C. Kaliszyk. “Matching concepts across HOL libraries”. in: CICM. ed. by S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban. vol. 8543. LNCS. Springer Verlag, 2014, 267–281. doi: .[GK15]
T. Gauthier and C. Kaliszyk. “Sharing HOL4 and HOL Light Proof Knowledge”. in: LPAR. ed. by M. Davis, A. Fehnker, A. McIver, and A. Voronkov. vol. 9450. LNCS. Springer, 2015, 372–386. doi: .[GKU16]
T. Gauthier, C. Kaliszyk, and J. Urban. “Initial Experiments with Statistical Conjecturing over Large Formal Corpora”. in: Work in Progress at CICM 2016. ed. by A. Kohlhase et al.. vol. 1785. CEUR. CEUR-WS.org, 2016, 219–228.[Gon+13]
G. Gonthier et al.. “A Machine-Checked Proof of the Odd Order Theorem”. in: Interactive Theorem Proving. ed. by S. Blazy, C. Paulin-Mohring, and D. Pichardie. 2013, 163–179.[Hal+15b]
T. C. Hales et al.. “A formal proof of the Kepler conjecture”. in: CoRR abs/1501.02155 (2015). url: .[HHP93b]
R. Harper, F. Honsell, and G. Plotkin. “A framework for defining logics”. in: Journal of the Association for Computing Machinery 40.1 (1993), 143–184.[HKR12a]
F. Horozal, M. Kohlhase, and F. Rabe. “Extending MKM Formats at the Statement Level”. in: Intelligent Computer Mathematics. ed. by J. Campbell, J. Carette, G. Dos Reis, J. Jeuring, P. Sojka, V. Sorge, and M. Wenzel. Springer, 2012, 64–79.[HKR12b]
F. Horozal, M. Kohlhase, and F. Rabe. “Extending MKM Formats at the Statement Level”. in: Intelligent Computer Mathematics. Conferences on Intelligent Computer Mathematics (CICM) (Bremen, Germany, July 9–14, 2012). ed. by J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge. LNAI 7362. Berlin and Heidelberg: Springer Verlag, 2012, 65–80. url: .[HKR14]
F. Horozal, M. Kohlhase, and F. Rabe. “Flexary Operators for Formalized Mathematics”. in: Intelligent Computer Mathematics 2014. Conferences on Intelligent Computer Mathematics (Coimbra, Portugal, July 7–11, 2014). ed. by S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban. LNCS 8543. Springer, 2014, 312–327. url: .[Hor14]
F. Horozal. “A Framework for Defining Declarative Languages”. PhD thesis. Jacobs University Bremen, Nov. 2014. url: .[How80]
W. Howard. “The formulas-as-types notion of construction”. in: To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism. Academic Press, 1980, 479–490.[HS02]
M. Hofmann and T. Streicher. “The Groupoid Interpretation of Type Theory”. in: (Apr. 2002).[Ian+13]
M. Iancu, M. Kohlhase, F. Rabe, and J. Urban. “The Mizar Mathematical Library in OMDoc: Translation and Applications”. in: Journal of Automated Reasoning 50.2 (2013), 191–202.[Ian+14]
M. Iancu, C. Jucovschi, M. Kohlhase, and T. Wiesing. “System Description: MathHub.info”. in: Intelligent Computer Mathematics. ed. by S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban. Springer, 2014, 431–434.[Ian17]
M. Iancu. “Towards Flexiformal Mathematics”. PhD thesis. Bremen, Germany: Jacobs University, 2017. url: .[Jeu+12]
J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge, eds.. Intelligent Computer Mathematics. Conferences on Intelligent Computer Mathematics (CICM) (Bremen, Germany, July 9–14, 2012). LNAI 7362. Berlin and Heidelberg: Springer Verlag, 2012.[KK13a]
C. Kaliszyk and A. Krauss. “Scalable LCF-style proof translation”. in: Interactive Theorem Proving. ed. by S. Blazy, C. Paulin-Mohring, and D. Pichardie. Springer, 2013, 51–66.[KK13b]
C. Kaliszyk and A. Krauss. “Scalable LCF-style proof translation”. in: ITP. ed. by S. Blazy, C. Paulin-Mohring, and D. Pichardie. vol. 7998. LNCS. Springer Verlag, 2013, 51–66.[Koh08]
M. Kohlhase. “Using L
A
T
E
X as a Semantic Markup Format”. in: Mathematics in Computer Science 2.2 (2008), 279–304.[Koh13a]
M. Kohlhase. “The Flexiformalist Manifesto”. in: 14th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2012). ed. by A. Voronkov, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. M. Watt, and D. Zaharie. Timisoara, Romania: IEEE Press, 2013, 30–36. url: .[Koh14]
M. Kohlhase. “Mathematical Knowledge Management: Transcending the One-Brain-Barrier with Theory Graphs”. in: EMS Newsletter (June 2014), 22–27. url: .[KP93]
M. Kohlhase and F. Pfenning. “Unification in a -Calculus with Intersection Types”. in: Proceedings of the International Logic Programming Symposion ILPS’93. ed. by D. Miller. MIT Press, 1993, 488–505. url: .[KR14]
C. Kaliszyk and F. Rabe. “Towards Knowledge Management for HOL Light”. in: Intelligent Computer Mathematics. ed. by S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban. Springer, 2014, 357–372.[KR16a]
M. Kohlhase and F. Rabe. “QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge”. in: Journal of Formalized Reasoning 9.1 (2016), 201–234.[KR16b]
M. Kohlhase and F. Rabe. “QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge”. in: Journal of Formalized Reasoning 9.1 (2016), 201–234. url: .[KRSC11]
M. Kohlhase, F. Rabe, and C. Sacerdoti Coen. “A Foundational View on Integration Problems”. in: Intelligent Computer Mathematics. ed. by J. Davenport, W. Farmer, F. Rabe, and J. Urban. LNAI 6824. Springer Verlag, 2011, 107–122. url: .[KŞ06]
M. Kohlhase and I. Şucan. “A Search Engine for Mathematical Formulae”. in: Artificial Intelligence and Symbolic Computation. ed. by T. Ida, J. Calmet, and D. Wang. Springer, 2006, 241–253.[KS10]
A. Krauss and A. Schropp. “A Mechanized Translation from Higher-Order Logic to Set Theory”. in: Interactive Theorem Proving. ed. by M. Kaufmann and L. Paulson. Springer, 2010, 323–338.[KU15]
C. Kaliszyk and J. Urban. “HOL(y)Hammer: Online ATP Service for HOL Light”. in: Mathematics in Computer Science 9.1 (2015), 5–22.[KW03]
H. Kanayama and H. Watanabe. “Multilingual translation via annotated hub language”. in: MT-Summit IX. 2003, 202–207.[KW10]
C. Keller and B. Werner. “Importing HOL Light into Coq”. in: Interactive Theorem Proving. ed. by M. Kaufmann and L. Paulson. Springer, 2010, 307–322.[Luo09]
Z. Luo. “Manifest Fields and Module Mechanisms in Intensional Type Theory”. in: Types for Proofs and Programs. ed. by S. Berardi, F. Damiani, and U. de’Liguoro. Berlin, Heidelberg: Springer Berlin Heidelberg, 2009, 237–255.[ML74]
P. Martin-Löf. “An Intuitionistic Theory of Types: Predicative Part”. in: Proceedings of the ’73 Logic Colloquium. North-Holland, 1974, 73–118.[ML94]
P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1994.[NK07]
I. Normann and M. Kohlhase. “Extended Formula Normalization for -Retrieval and Sharing of Mathematical Knowledge”. in: Towards Mechanized Mathematical Assistants. MKM/Calculemus. ed. by M. Kauers, M. Kerber, R. Miner, and W. Windsteiger. LNAI 4573. Springer Verlag, 2007, 266–279.[Nor08]
I. Normann. “Automated Theory Interpretation”. PhD thesis. Bremen, Germany: Jacobs University, 2008. url: .[NSM01]
P. Naumov, M. Stehr, and J. Meseguer. “The HOL/NuPRL proof translator - a practical approach to formal interoperability”. in: 14th International Conference on Theorem Proving in Higher Order Logics. ed. by R. Boulton and P. Jackson. Springer, 2001.[OS06a]
S. Obua and S. Skalberg. “Importing HOL into Isabelle/HOL”. in: Automated Reasoning. ed. by N. Shankar and U. Furbach. vol. 4130. Springer, 2006.[OS06b]
S. Obua and S. Skalberg. “Importing HOL into Isabelle/HOL”. in: Automated Reasoning: Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings. ed. by U. Furbach and N. Shankar. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, 298–302. doi: .[Pfe01]
F. Pfenning. “Logical frameworks”. in: Handbook of automated reasoning. ed. by J. Robinson and A. Voronkov. Elsevier, 2001, 1063–1147.[Pfe+03]
F. Pfenning, C. Schürmann, M. Kohlhase, N. Shankar, and S. Owre.. The Logosphere Project. . 2003.[Pfe93]
F. Pfenning. “Refinement Types for Logical Frameworks”. in: Informal Proceedings of the 1993 Workshop on Types for Proofs and Programs. ed. by H. Geuvers. Nijmegen, The Netherlands: University of Nijmegen, May 1993, 285–301.[Rab12]
F. Rabe. “A Query Language for Formal Mathematical Libraries”. in: Intelligent Computer Mathematics. Conferences on Intelligent Computer Mathematics (CICM) (Bremen, Germany, July 9–14, 2012). ed. by J. Jeuring, J. A. Campbell, J. Carette, G. Dos Reis, P. Sojka, M. Wenzel, and V. Sorge. LNAI 7362. Berlin and Heidelberg: Springer Verlag, 2012, 142–157. arXiv: [cs.LO].[Rab17a]
F. Rabe. “A Modular Type Reconstruction Algorithm”. in: ACM Transactions on Computational Logic (2017). accepted pending minor revision; see .[Rab17b]
F. Rabe. “How to Identify, Translate, and Combine Logics?”. in: Journal of Logic and Computation 27.6 (2017), 1753–1798.[RK13b]
F. Rabe and M. Kohlhase. “A Scalable Module System”. in: Information & Computation 0.230 (2013), 1–54. url: .[RKS11]
F. Rabe, M. Kohlhase, and C. Sacerdoti Coen. “A Foundational View on Integration Problems”. in: Intelligent Computer Mathematics. ed. by J. Davenport, W. Farmer, F. Rabe, and J. Urban. Springer, 2011, 107–122.[Sol95]
R. Solomon. “On Finite Simple Groups and Their Classification”. in: Notices of the AMS (Feb. 1995), 231–239.[SS89]
M. Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations. LNAI 395. Springer Verlag, 1989.[Sto+17]
C. Stolze, L. Liquori, F. Honsell, and I. Scagnetto. “Towards a Logical Framework with Intersection and Union Types”. in: 11th International Workshop on Logical Frameworks and Meta-languages, LFMTP. Oxford, United Kingdom, Sept. 2017, 1 –9. url: .[SW11]
B. Spitters and E. van der Weegen. “Type Classes for Mathematics in Type Theory”. in: CoRR abs/1102.1323 (2011). arXiv: . url: .[Uni13]
T. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: , 2013.[Wat+14]
S. Watt, J. Davenport, A. Sexton, P. Sojka, and J. Urban, eds.. Intelligent Computer Mathematics. Conferences on Intelligent Computer Mathematics (Coimbra, Portugal, July 7–11, 2014). LNCS 8543. Springer, 2014.[Wie06]
F. Wiedijk. The Seventeen Provers of the World. Springer, 2006.[Wie92]
G. Wiederhold. “Mediators in the architecture of future information systems”. in: Computer 25.3 (1992), 38–49.[WKR17]
T. Wiesing, M. Kohlhase, and F. Rabe. “Virtual Theories – A Uniform Interface to Mathematical Knowledge Bases”. in: MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences. ed. by J. Blömer, T. Kutsia, and D. Simos. LNCS 10693. Springer Verlag, 2017, 243–257. url: .[WR13]
A. Whitehead and B. Russell. Principia Mathematica. Cambridge University Press, 1913.